Theory Smooth
section ‹Smooth Functions between Normed Vector Spaces›
theory Smooth
imports
Analysis_More
begin
subsection ‹From/To ‹Multivariate_Taylor.thy››
lemma multivariate_Taylor_integral:
fixes f::"'a::real_normed_vector ⇒ 'b::banach"
and Df::"'a ⇒ nat ⇒ 'a ⇒ 'b"
assumes "n > 0"
assumes Df_Nil: "⋀a x. Df a 0 H = f a"
assumes Df_Cons: "⋀a i d. a ∈ closed_segment X (X + H) ⟹ i < n ⟹
((λa. Df a i H) has_derivative (Df a (Suc i))) (at a within G)"
assumes cs: "closed_segment X (X + H) ⊆ G"
defines "i ≡ λx.
((1 - x) ^ (n - 1) / fact (n - 1)) *⇩R Df (X + x *⇩R H) n H"
shows multivariate_Taylor_has_integral:
"(i has_integral f (X + H) - (∑i<n. (1 / fact i) *⇩R Df X i H)) {0..1}"
and multivariate_Taylor:
"f (X + H) = (∑i<n. (1 / fact i) *⇩R Df X i H) + integral {0..1} i"
and multivariate_Taylor_integrable:
"i integrable_on {0..1}"
proof goal_cases
case 1
let ?G = "closed_segment X (X + H)"
define line where "line t = X + t *⇩R H" for t
have segment_eq: "closed_segment X (X + H) = line ` {0 .. 1}"
by (auto simp: line_def closed_segment_def algebra_simps)
have line_deriv: "⋀x. (line has_derivative (λt. t *⇩R H)) (at x)"
by (auto intro!: derivative_eq_intros simp: line_def [abs_def])
define g where "g = f o line"
define Dg where "Dg n t = Df (line t) n H" for n :: nat and t :: real
note ‹n > 0›
moreover
have Dg0: "Dg 0 = g" by (auto simp add: Dg_def Df_Nil g_def)
moreover
have DgSuc: "(Dg m has_vector_derivative Dg (Suc m) t) (at t within {0..1})"
if "m < n" "0 ≤ t" "t ≤ 1" for m::nat and t::real
proof -
from that have [intro]: "line t ∈ ?G" using assms
by (auto simp: segment_eq)
note [derivative_intros] = has_derivative_in_compose[OF _ has_derivative_subset[OF Df_Cons]]
interpret Df: linear "(λd. Df (line t) (Suc m) d)"
by (auto intro!: has_derivative_linear derivative_intros ‹m < n›)
note [derivative_intros] =
has_derivative_compose[OF _ line_deriv]
show ?thesis
using Df.scaleR ‹m < n›
by (auto simp: Dg_def [abs_def] has_vector_derivative_def g_def segment_eq
intro!: derivative_eq_intros subsetD[OF cs])
qed
ultimately
have g_Taylor: "(i has_integral g 1 - (∑i<n. ((1 - 0) ^ i / fact i) *⇩R Dg i 0)) {0 .. 1}"
unfolding i_def Dg_def [abs_def] line_def
by (rule Taylor_has_integral) auto
then show c: ?case using ‹n > 0› by (auto simp: g_def line_def Dg_def)
case 2 show ?case using c
by (simp add: integral_unique add.commute)
case 3 show ?case using c by force
qed
subsection ‹Higher-order differentiable›
fun higher_differentiable_on ::
"'a::real_normed_vector set ⇒ ('a ⇒ 'b::real_normed_vector) ⇒ nat ⇒ bool" where
"higher_differentiable_on S f 0 ⟷ continuous_on S f"
| "higher_differentiable_on S f (Suc n) ⟷
(∀x∈S. f differentiable (at x)) ∧
(∀v. higher_differentiable_on S (λx. frechet_derivative f (at x) v) n)"
lemma ball_differentiable_atD: "∀x∈S. f differentiable at x ⟹ f differentiable_on S"
by (auto simp: differentiable_on_def differentiable_at_withinI)
lemma higher_differentiable_on_imp_continuous_on:
"continuous_on S f" if "higher_differentiable_on S f n"
using that
by (cases n) (auto simp: differentiable_imp_continuous_on ball_differentiable_atD)
lemma higher_differentiable_on_imp_differentiable_on:
"f differentiable_on S" if "higher_differentiable_on S f k" "k > 0"
using that
by (cases k) (auto simp: ball_differentiable_atD)
lemma higher_differentiable_on_congI:
assumes "open S" "higher_differentiable_on S g n"
and "⋀x. x ∈ S ⟹ f x = g x"
shows "higher_differentiable_on S f n"
using assms(2,3)
proof (induction n arbitrary: f g)
case 0
then show ?case by auto
next
case (Suc n)
have 1: "∀x∈S. g differentiable (at x)" and
2: "higher_differentiable_on S (λx. frechet_derivative g (at x) v) n" for v
using Suc by auto
have 3: "∀x∈S. f differentiable (at x)" using 1 Suc(3) assms(1)
by (metis differentiable_eqI)
have 4: "frechet_derivative f (at x) v = frechet_derivative g (at x) v" if "x ∈ S" for x v
using "3" Suc.prems(2) assms(1) frechet_derivative_transform_within_open_ext that by blast
from 2 3 4 show ?case
using Suc.IH[OF 2 4] by auto
qed
lemma higher_differentiable_on_cong:
assumes "open S" "S = T"
and "⋀x. x ∈ T ⟹ f x = g x"
shows "higher_differentiable_on S f n ⟷ higher_differentiable_on T g n"
using higher_differentiable_on_congI assms by auto
lemma higher_differentiable_on_SucD:
"higher_differentiable_on S f n" if "higher_differentiable_on S f (Suc n)"
using that
by (induction n arbitrary: f) (auto simp: differentiable_imp_continuous_on ball_differentiable_atD)
lemma higher_differentiable_on_addD:
"higher_differentiable_on S f n" if "higher_differentiable_on S f (n + m)"
using that
by (induction m arbitrary: f n)
(auto simp del: higher_differentiable_on.simps dest!: higher_differentiable_on_SucD)
lemma higher_differentiable_on_le:
"higher_differentiable_on S f n" if "higher_differentiable_on S f m" "n ≤ m"
using higher_differentiable_on_addD[of S f n "m - n"] that
by auto
lemma higher_differentiable_on_open_subsetsI:
"higher_differentiable_on S f n"
if "⋀x. x ∈ S ⟹ ∃T. x ∈ T ∧ open T ∧ higher_differentiable_on T f n"
using that
proof (induction n arbitrary: f)
case 0
show ?case
by (force simp: continuous_on_def
dest!: 0
dest: at_within_open
intro!: Lim_at_imp_Lim_at_within[where S=S])
next
case (Suc n)
have "f differentiable at x" if "x ∈ S" for x
using Suc.prems[OF ‹x ∈ S›]
by (auto simp: differentiable_on_def dest: at_within_open dest!: bspec)
then have "f differentiable_on S"
by (auto simp: differentiable_on_def intro!: differentiable_at_withinI[where s=S])
with Suc show ?case
by fastforce
qed
lemma higher_differentiable_on_const: "higher_differentiable_on S (λx. c) n"
by (induction n arbitrary: c) (auto simp: continuous_intros frechet_derivative_const)
lemma higher_differentiable_on_id: "higher_differentiable_on S (λx. x) n"
by (cases n) (auto simp: frechet_derivative_works higher_differentiable_on_const)
lemma higher_differentiable_on_add:
"higher_differentiable_on S (λx. f x + g x) n"
if "higher_differentiable_on S f n"
"higher_differentiable_on S g n"
"open S"
using that
proof (induction n arbitrary: f g)
case 0
then show ?case by (auto intro!: continuous_intros)
next
case (Suc n)
from Suc.prems have
f: "⋀x. x∈S ⟹ f differentiable (at x)"
and hf: "higher_differentiable_on S (λx. frechet_derivative f (at x) v) n"
and g: "⋀x. x∈S ⟹ g differentiable (at x)"
and hg: "higher_differentiable_on S (λx. frechet_derivative g (at x) v) n"
for v
by auto
show ?case
using f g ‹open S›
by (auto simp: frechet_derivative_plus
intro!: derivative_intros f g Suc.IH hf hg
cong: higher_differentiable_on_cong)
qed
lemma (in bounded_bilinear) differentiable:
"(λx. prod (f x) (g x)) differentiable at x within S"
if "f differentiable at x within S"
"g differentiable at x within S"
by (blast intro: differentiableI frechet_derivative_worksI that FDERIV)
context begin
private lemmas d = bounded_bilinear.differentiable
lemmas differentiable_inner = bounded_bilinear_inner[THEN d]
and differentiable_scaleR = bounded_bilinear_scaleR[THEN d]
and differentiable_mult = bounded_bilinear_mult[THEN d]
end
lemma (in bounded_bilinear) differentiable_on:
"(λx. prod (f x) (g x)) differentiable_on S"
if "f differentiable_on S" "g differentiable_on S"
using that by (auto simp: differentiable_on_def differentiable)
context begin
private lemmas do = bounded_bilinear.differentiable_on
lemmas differentiable_on_inner = bounded_bilinear_inner[THEN do]
and differentiable_on_scaleR = bounded_bilinear_scaleR[THEN do]
and differentiable_on_mult = bounded_bilinear_mult[THEN do]
end
lemma (in bounded_bilinear) higher_differentiable_on:
"higher_differentiable_on S (λx. prod (f x) (g x)) n"
if
"higher_differentiable_on S f n"
"higher_differentiable_on S g n"
"open S"
using that
proof (induction n arbitrary: f g)
case 0
then show ?case by (auto intro!: continuous_intros continuous_on)
next
case (Suc n)
from Suc.prems have
f: "⋀x. x∈S ⟹ f differentiable (at x)"
and hf: "higher_differentiable_on S (λx. frechet_derivative f (at x) v) n"
and g: "⋀x. x∈S ⟹ g differentiable (at x)"
and hg: "higher_differentiable_on S (λx. frechet_derivative g (at x) v) n"
for v
by auto
show ?case
using f g ‹open S› Suc
by (auto simp: frechet_derivative
intro!: derivative_intros f g differentiable higher_differentiable_on_add Suc.IH
intro: higher_differentiable_on_SucD
cong: higher_differentiable_on_cong)
qed
context begin
private lemmas hdo = bounded_bilinear.higher_differentiable_on
lemmas higher_differentiable_on_inner = bounded_bilinear_inner[THEN hdo]
and higher_differentiable_on_scaleR = bounded_bilinear_scaleR[THEN hdo]
and higher_differentiable_on_mult = bounded_bilinear_mult[THEN hdo]
end
lemma higher_differentiable_on_sum:
"higher_differentiable_on S (λx. ∑i∈F. f i x) n"
if "⋀i. i ∈ F ⟹ finite F ⟹ higher_differentiable_on S (f i) n" "open S"
using that
by (induction F rule: infinite_finite_induct)
(auto intro!: higher_differentiable_on_const higher_differentiable_on_add)
lemma higher_differentiable_on_subset:
"higher_differentiable_on S f n"
if "higher_differentiable_on T f n" "S ⊆ T"
using that
by (induction n arbitrary: f) (auto intro: continuous_on_subset differentiable_on_subset)
lemma higher_differentiable_on_compose:
"higher_differentiable_on S (f o g) n"
if "higher_differentiable_on T f n" "higher_differentiable_on S g n" "g ` S ⊆ T" "open S" "open T"
for g::"_⇒_::euclidean_space"
using that(1-3)
proof (induction n arbitrary: f g)
case 0
then show ?case using that(4-)
by (auto simp: continuous_on_compose2)
next
case (Suc n)
from Suc.prems
have
f: "⋀x. x ∈ T ⟹ f differentiable (at x)"
and g: "⋀x. x ∈ S ⟹ g differentiable (at x)"
and hf: "higher_differentiable_on T (λx. frechet_derivative f (at x) v) n"
and hg: "higher_differentiable_on S (λx. frechet_derivative g (at x) w) n"
for v w
by auto
show ?case
using ‹g ` _ ⊆ _› ‹open S› f g ‹open T› Suc
Suc.IH[where f="λx. frechet_derivative f (at x) v"
and g = "λx. g x" for v, unfolded o_def]
higher_differentiable_on_SucD[OF Suc.prems(2)]
by (auto
simp: frechet_derivative_compose_eucl subset_iff
simp del: o_apply
intro!: differentiable_chain_within higher_differentiable_on_sum
higher_differentiable_on_scaleR higher_differentiable_on_inner
higher_differentiable_on_const
intro: differentiable_at_withinI
cong: higher_differentiable_on_cong)
qed
lemma higher_differentiable_on_uminus:
"higher_differentiable_on S (λx. - f x) n"
if "higher_differentiable_on S f n" "open S"
using higher_differentiable_on_scaleR[of S "λx. -1" n f] that
by (auto simp: higher_differentiable_on_const)
lemma higher_differentiable_on_minus:
"higher_differentiable_on S (λx. f x - g x) n"
if "higher_differentiable_on S f n"
"higher_differentiable_on S g n"
"open S"
using higher_differentiable_on_add[OF _ higher_differentiable_on_uminus, OF that(1,2,3,3)]
by simp
lemma higher_differentiable_on_inverse:
"higher_differentiable_on S (λx. inverse (f x)) n"
if "higher_differentiable_on S f n" "0 ∉ f ` S" "open S"
for f::"_⇒_::real_normed_field"
using that
proof (induction n arbitrary: f)
case 0
then show ?case by (auto simp: continuous_on_inverse)
next
case (Suc n)
from Suc.prems(1) have fn: "higher_differentiable_on S f n" by (rule higher_differentiable_on_SucD)
from Suc show ?case
by (auto simp: continuous_on_inverse image_iff power2_eq_square
frechet_derivative_inverse divide_inverse
intro!: differentiable_inverse higher_differentiable_on_uminus higher_differentiable_on_mult
Suc.IH fn
cong: higher_differentiable_on_cong)
qed
lemma higher_differentiable_on_divide:
"higher_differentiable_on S (λx. f x / g x) n"
if
"higher_differentiable_on S f n"
"higher_differentiable_on S g n"
"⋀x. x ∈ S ⟹ g x ≠ 0"
"open S"
for f::"_⇒_::real_normed_field"
using higher_differentiable_on_mult[OF _ higher_differentiable_on_inverse, OF that(1,2) _ that(4,4)]
that(3)
by (auto simp: divide_inverse image_iff)
lemma differentiable_on_open_Union:
"f differentiable_on ⋃S"
if "⋀s. s ∈ S ⟹ f differentiable_on s"
"⋀s. s ∈ S ⟹ open s"
using that
unfolding differentiable_on_def
by (metis Union_iff at_within_open open_Union)
lemma higher_differentiable_on_open_Union: "higher_differentiable_on (⋃S) f n"
if "⋀s. s ∈ S ⟹ higher_differentiable_on s f n"
"⋀s. s ∈ S ⟹ open s"
using that
proof (induction n arbitrary: f)
case 0
then show ?case by (auto simp: continuous_on_open_Union)
next
case (Suc n)
then show ?case
by (auto simp: differentiable_on_open_Union)
qed
lemma differentiable_on_open_Un:
"f differentiable_on S ∪ T"
if "f differentiable_on S"
"f differentiable_on T"
"open S" "open T"
using that differentiable_on_open_Union[of "{S, T}" f]
by auto
lemma higher_differentiable_on_open_Un: "higher_differentiable_on (S ∪ T) f n"
if "higher_differentiable_on S f n"
"higher_differentiable_on T f n"
"open S" "open T"
using higher_differentiable_on_open_Union[of "{S, T}" f n] that
by auto
lemma higher_differentiable_on_sqrt: "higher_differentiable_on S (λx. sqrt (f x)) n"
if "higher_differentiable_on S f n" "0 ∉ f ` S" "open S"
using that
proof (induction n arbitrary: f)
case 0
then show ?case by (auto simp: continuous_intros)
next
case (Suc n)
from Suc.prems(1) have fn: "higher_differentiable_on S f n" by (rule higher_differentiable_on_SucD)
then have "continuous_on S f"
by (rule higher_differentiable_on_imp_continuous_on)
with ‹open S› have op: "open (S ∩ f -` {0<..})" (is "open ?op")
by (rule open_continuous_vimage') simp
from ‹open S› ‹continuous_on S f› have on: "open (S ∩ f -` {..<0})" (is "open ?on")
by (rule open_continuous_vimage') simp
have op': "higher_differentiable_on ?op (λx. 1) n" and on': "higher_differentiable_on ?on (λx. -1) n"
by (rule higher_differentiable_on_const)+
then have i: "higher_differentiable_on (?op ∪ ?on) (λx. if 0 < f x then 1::real else - 1) n"
by (auto intro!: higher_differentiable_on_open_Un op on
higher_differentiable_on_congI[OF _ op'] higher_differentiable_on_congI[OF _ on'])
also have "?op ∪ ?on = S" using Suc by auto
finally have i: "higher_differentiable_on S (λx. if 0 < f x then 1::real else - 1) n" .
from fn i Suc show ?case
by (auto simp: sqrt_differentiable_on image_iff frechet_derivative_sqrt
intro!: sqrt_differentiable higher_differentiable_on_mult higher_differentiable_on_inverse
higher_differentiable_on_divide higher_differentiable_on_const
cong: higher_differentiable_on_cong)
qed
lemma higher_differentiable_on_frechet_derivativeI:
"higher_differentiable_on X (λx. frechet_derivative f (at x) h) i"
if "higher_differentiable_on X f (Suc i)" "open X" "x ∈ X"
using that(1)
by (induction i arbitrary: f h) auto
lemma higher_differentiable_on_norm:
"higher_differentiable_on S (λx. norm (f x)) n"
if "higher_differentiable_on S f n" "0 ∉ f ` S" "open S"
for f::"_⇒_::real_inner"
using that
proof (induction n arbitrary: f)
case 0
then show ?case by (auto simp: continuous_on_norm)
next
case (Suc n)
from Suc.prems(1) have fn: "higher_differentiable_on S f n" by (rule higher_differentiable_on_SucD)
from Suc show ?case
by (auto simp: continuous_on_norm frechet_derivative_norm image_iff sgn_div_norm
cong: higher_differentiable_on_cong
intro!: differentiable_norm_compose_at higher_differentiable_on_inner
higher_differentiable_on_inverse
higher_differentiable_on_mult Suc.IH fn)
qed
declare higher_differentiable_on.simps [simp del]
lemma higher_differentiable_on_Pair:
"higher_differentiable_on S f k ⟹ higher_differentiable_on S g k ⟹
higher_differentiable_on S (λx. (f x, g x)) k"
if "open S"
proof (induction k arbitrary: f g)
case 0
then show ?case
unfolding higher_differentiable_on.simps
by (auto intro!: continuous_intros)
next
case (Suc k)
then show ?case using that
unfolding higher_differentiable_on.simps
by (auto simp: frechet_derivative_pair[of f _ g] cong: higher_differentiable_on_cong)
qed
lemma higher_differentiable_on_compose':
"higher_differentiable_on S (λx. f (g x)) n"
if "higher_differentiable_on T f n" "higher_differentiable_on S g n" "g ` S ⊆ T" "open S" "open T"
for g::"_⇒_::euclidean_space"
using higher_differentiable_on_compose[of T f n S g] comp_def that
by (metis (no_types, lifting) higher_differentiable_on_cong)
lemma higher_differentiable_on_fst:
"higher_differentiable_on (S × T) fst k"
proof (induction k)
case (Suc k)
then show ?case
unfolding higher_differentiable_on.simps
by (auto simp: differentiable_at_fst frechet_derivative_fst frechet_derivative_id higher_differentiable_on_const)
qed (auto simp: higher_differentiable_on.simps continuous_on_fst)
lemma higher_differentiable_on_snd:
"higher_differentiable_on (S × T) snd k"
proof (induction k)
case (Suc k)
then show ?case
unfolding higher_differentiable_on.simps
by (auto intro!: continuous_intros
simp: differentiable_at_snd frechet_derivative_snd frechet_derivative_id higher_differentiable_on_const)
qed (auto simp: higher_differentiable_on.simps continuous_on_snd)
lemma higher_differentiable_on_fst_comp:
"higher_differentiable_on S (λx. fst (f x)) k"
if "higher_differentiable_on S f k" "open S"
using that
by (induction k arbitrary: f)
(auto intro!: continuous_intros differentiable_at_fst
cong: higher_differentiable_on_cong
simp: higher_differentiable_on.simps frechet_derivative_fst)
lemma higher_differentiable_on_snd_comp:
"higher_differentiable_on S (λx. snd (f x)) k"
if "higher_differentiable_on S f k" "open S"
using that
by (induction k arbitrary: f)
(auto intro!: continuous_intros differentiable_at_snd
cong: higher_differentiable_on_cong
simp: higher_differentiable_on.simps frechet_derivative_snd)
lemma higher_differentiable_on_Pair':
"higher_differentiable_on S f k ⟹ higher_differentiable_on T g k ⟹
higher_differentiable_on (S × T) (λx. (f (fst x), g (snd x))) k"
if S: "open S" and T: "open T"
for f::"_::euclidean_space⇒_" and g::"_::euclidean_space⇒_"
by (auto intro!: higher_differentiable_on_Pair open_Times S T
higher_differentiable_on_fst
higher_differentiable_on_snd
higher_differentiable_on_compose'[where f=f and T=S]
higher_differentiable_on_compose'[where f=g and T=T])
lemma higher_differentiable_on_sin: "higher_differentiable_on S (λx. sin (f x::real)) n"
and higher_differentiable_on_cos: "higher_differentiable_on S (λx. cos (f x::real)) n"
if f: "higher_differentiable_on S f n" and S: "open S"
unfolding atomize_conj
using f
proof (induction n)
case (Suc n)
then have "higher_differentiable_on S f n"
"higher_differentiable_on S (λx. sin (f x)) n"
"higher_differentiable_on S (λx. cos (f x)) n"
"⋀x. x ∈ S ⟹ f differentiable at x"
using higher_differentiable_on_SucD
by (auto simp: higher_differentiable_on.simps)
with Suc show ?case
by (auto simp: higher_differentiable_on.simps sin_differentiable_at cos_differentiable_at
frechet_derivative_sin frechet_derivative_cos S
intro!: higher_differentiable_on_mult higher_differentiable_on_uminus
cong: higher_differentiable_on_cong[OF S])
qed (auto simp: higher_differentiable_on.simps intro!: continuous_intros)
subsection ‹Higher directional derivatives›
primrec nth_derivative :: "nat ⇒ ('a::real_normed_vector ⇒ 'b::real_normed_vector) ⇒ 'a ⇒ 'a ⇒ 'b" where
"nth_derivative 0 f x h = f x"
| "nth_derivative (Suc i) f x h = nth_derivative i (λx. frechet_derivative f (at x) h) x h"
lemma frechet_derivative_nth_derivative_commute:
"frechet_derivative (λx. nth_derivative i f x h) (at x) h =
nth_derivative i (λx. frechet_derivative f (at x) h) x h"
by (induction i arbitrary: f) auto
lemma nth_derivative_funpow:
"nth_derivative i f x h = ((λf x. frechet_derivative f (at x) h) ^^ i) f x"
by (induction i arbitrary: f) (auto simp del: funpow.simps simp: funpow_Suc_right)
lemma nth_derivative_exists:
"∃f'. ((λx. nth_derivative i f x h) has_derivative f') (at x) ∧
f' h = nth_derivative (Suc i) f x h"
if "higher_differentiable_on X f (Suc i)" "open X" "x ∈ X"
using that(1)
proof (induction i arbitrary: f)
case 0
with that show ?case
by (auto simp: higher_differentiable_on.simps that dest!: frechet_derivative_worksI)
next
case (Suc i)
from Suc.prems
have "⋀x. x ∈ X ⟹ f differentiable at x" "higher_differentiable_on X (λx. frechet_derivative f (at x) h) (Suc i)"
unfolding higher_differentiable_on.simps(2)[where n = "Suc i"]
by auto
from Suc.IH[OF this(2)] show ?case
by auto
qed
lemma higher_derivatives_exists:
assumes "higher_differentiable_on X f n" "open X"
obtains Df where
"⋀a h. Df a 0 h = f a"
"⋀a h i. i < n ⟹ a ∈ X ⟹ ((λa. Df a i H) has_derivative Df a (Suc i)) (at a)"
"⋀a i. i ≤ n ⟹ a ∈ X ⟹ Df a i H = nth_derivative i f a H"
proof -
have "higher_differentiable_on X f (Suc i)" if "i < n" for i
apply (rule higher_differentiable_on_le[OF assms(1)])
using that by simp
from nth_derivative_exists[OF this assms(2)]
have "∀i∈{..<n}. ∀x ∈ X. ∃f'. ((λx. nth_derivative i f x H) has_derivative f') (at x) ∧ f' H = nth_derivative (Suc i) f x H"
by blast
from this[unfolded bchoice_iff]
obtain f' where f': "i < n ⟹ x ∈ X ⟹ ((λx. nth_derivative i f x H) has_derivative f' x i) (at x)"
"i < n ⟹ x ∈ X ⟹ f' x i H = nth_derivative (Suc i) f x H" for x i
by force
define Df where "Df a i h = (if i = 0 then f a else f' a (i - 1) h)" for a i h
have "Df a 0 h = f a" for a h
by (auto simp: Df_def)
moreover have "i < n ⟹ a ∈ X ⟹ ((λa. Df a i H) has_derivative Df a (Suc i)) (at a)"
for i a
apply (auto simp: Df_def[abs_def])
using _ ‹open X›
apply (rule has_derivative_transform_within_open)
apply (rule f')
apply (auto simp: f')
done
moreover have "i ≤ n ⟹ a ∈ X ⟹ Df a i H = nth_derivative i f a H" for i a
by (auto simp: Df_def f')
ultimately show ?thesis ..
qed
lemma nth_derivative_differentiable:
assumes "higher_differentiable_on S f (Suc n)" "x ∈ S"
shows "(λx. nth_derivative n f x v) differentiable at x"
using assms
by (induction n arbitrary: f) (auto simp: higher_differentiable_on.simps)
lemma higher_differentiable_on_imp_continuous_nth_derivative:
assumes "higher_differentiable_on S f n"
shows "continuous_on S (λx. nth_derivative n f x v)"
using assms
by (induction n arbitrary: f) (auto simp: higher_differentiable_on.simps)
lemma frechet_derivative_at_real_eq_scaleR:
"frechet_derivative f (at x) v = v *⇩R frechet_derivative f (at x) 1"
if "f differentiable (at x)" "NO_MATCH 1 v"
by (simp add: frechet_derivative_eq_vector_derivative that)
lemma higher_differentiable_on_real_Suc:
"higher_differentiable_on S f (Suc n) ⟷
(∀x∈S. f differentiable (at x)) ∧
(higher_differentiable_on S (λx. frechet_derivative f (at x) 1) n)"
if "open S"
for S::"real set"
using ‹open S›
by (auto simp: higher_differentiable_on.simps frechet_derivative_at_real_eq_scaleR
intro!: higher_differentiable_on_scaleR higher_differentiable_on_const
cong: higher_differentiable_on_cong)
lemma higher_differentiable_on_real_SucI:
fixes S::"real set"
assumes
"⋀x. x ∈ S ⟹ (λx. nth_derivative n f x 1) differentiable at x"
"continuous_on S (λx. nth_derivative (Suc n) f x 1)"
"higher_differentiable_on S f n"
and o: "open S"
shows "higher_differentiable_on S f (Suc n)"
using assms
proof (induction n arbitrary: f)
case 0
then show ?case
by (auto simp: higher_differentiable_on_real_Suc higher_differentiable_on.simps(1) o)
qed (fastforce simp: higher_differentiable_on_real_Suc)
lemma higher_differentiable_on_real_Suc':
"open S ⟹ higher_differentiable_on S f (Suc n) ⟷
(∀v. continuous_on S (λx. nth_derivative (Suc n) f x 1)) ∧
(∀x∈S. ∀v. (λx. nth_derivative n f x 1) differentiable (at x)) ∧ higher_differentiable_on S f n"
for S::"real set"
apply (auto simp: nth_derivative_differentiable
dest: higher_differentiable_on_SucD
intro: higher_differentiable_on_real_SucI)
by (auto simp: higher_differentiable_on_real_Suc higher_differentiable_on.simps(1)
higher_differentiable_on_imp_continuous_nth_derivative)
lemma closed_segment_subsetD:
"0 ≤ x ⟹ x ≤ 1 ⟹ (X + x *⇩R H) ∈ S"
if "closed_segment X (X + H) ⊆ S"
using that
by (rule subsetD) (auto simp: closed_segment_def algebra_simps intro!: exI[where x=x])
lemma higher_differentiable_Taylor:
fixes f::"'a::real_normed_vector ⇒ 'b::banach"
and H::"'a"
and Df::"'a ⇒ nat ⇒ 'a ⇒ 'a ⇒ 'b"
assumes "n > 0"
assumes hd: "higher_differentiable_on S f n" "open S"
assumes cs: "closed_segment X (X + H) ⊆ S"
defines "i ≡ λx. ((1 - x) ^ (n - 1) / fact (n - 1)) *⇩R nth_derivative n f (X + x *⇩R H) H"
shows "(i has_integral f (X + H) - (∑i<n. (1 / fact i) *⇩R nth_derivative i f X H)) {0..1}" (is ?th1)
and "f (X + H) = (∑i<n. (1 / fact i) *⇩R nth_derivative i f X H) + integral {0..1} i" (is ?th2)
and "i integrable_on {0..1}" (is ?th3)
proof -
from higher_derivatives_exists[OF hd]
obtain Df where Df: "(⋀a h. Df a 0 h = f a)"
"(⋀a h i. i < n ⟹ a ∈ S ⟹ ((λa. Df a i H) has_derivative Df a (Suc i)) (at a))"
"⋀a i. i ≤ n ⟹ a ∈ S ⟹ Df a i H = nth_derivative i f a H"
by blast
from multivariate_Taylor_integral[OF ‹n > 0›, of Df H f X, OF Df(1,2)] cs
have mt: "((λx. ((1 - x) ^ (n - 1) / fact (n - 1)) *⇩R Df (X + x *⇩R H) n H) has_integral
f (X + H) - (∑i<n. (1 / fact i) *⇩R Df X i H))
{0..1}"
by force
from cs have "X ∈ S" by auto
show ?th1
apply (rule has_integral_eq_rhs)
unfolding i_def
using negligible_empty _ mt
apply (rule has_integral_spike)
using closed_segment_subsetD[OF cs]
by (auto simp: Df ‹X ∈ S›)
then show ?th2 ?th3
unfolding has_integral_iff
by auto
qed
lemma frechet_derivative_componentwise:
"frechet_derivative f (at a) v = (∑i∈Basis. (v ∙ i) * (frechet_derivative f (at a) i))"
if "f differentiable at a"
for f::"'a::euclidean_space ⇒ real"
proof -
have "linear (frechet_derivative f (at a))"
using that
by (rule linear_frechet_derivative)
from Linear_Algebra.linear_componentwise[OF this, of v 1]
show ?thesis
by simp
qed
lemma second_derivative_componentwise:
"nth_derivative 2 f a v =
(∑i∈Basis. (∑j∈Basis. frechet_derivative (λa. frechet_derivative f (at a) j) (at a) i * (v ∙ j)) * (v ∙ i))"
if "higher_differentiable_on S f 2" and S: "open S" "a ∈ S"
for f::"'a::euclidean_space ⇒ real"
proof -
have diff: "(λx. frechet_derivative f (at x) v) differentiable at a" for v
using that
by (auto simp: numeral_2_eq_2 higher_differentiable_on.simps differentiable_on_openD
dest!: spec[where x=v])
have d1: "x ∈ S ⟹ f differentiable at x" for x
using that
by (auto simp: numeral_2_eq_2 higher_differentiable_on.simps dest!: differentiable_on_openD)
have eq: "⋀x. x ∈ Basis ⟹
frechet_derivative
(λx. ∑i∈Basis. v ∙ i * frechet_derivative f (at x) i) (at a) x =
(∑j∈Basis. frechet_derivative (λa. frechet_derivative f (at a) j) (at a) x * (v ∙ j))"
apply (subst frechet_derivative_sum)
subgoal by (auto intro!: differentiable_mult diff)
apply (rule sum.cong)
apply simp
apply (subst frechet_derivative_times)
subgoal by simp
subgoal by (rule diff)
by (simp add: frechet_derivative_const)
show ?thesis
apply (simp add: numeral_2_eq_2)
apply (subst frechet_derivative_componentwise[OF diff])
apply (rule sum.cong)
apply simp
apply simp
apply (rule disjI2)
apply (rule trans)
apply (rule frechet_derivative_transform_within_open_ext [OF _ S frechet_derivative_componentwise])
apply (simp add: diff)
apply (rule d1, assumption)
apply (simp add: eq)
done
qed
lemma higher_differentiable_Taylor1:
fixes f::"'a::real_normed_vector ⇒ 'b::banach"
assumes hd: "higher_differentiable_on S f 2" "open S"
assumes cs: "closed_segment X (X + H) ⊆ S"
defines "i ≡ λx. ((1 - x)) *⇩R nth_derivative 2 f (X + x *⇩R H) H"
shows "(i has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1}"
and "f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} i"
and "i integrable_on {0..1}"
using higher_differentiable_Taylor[OF _ hd cs]
by (auto simp: numeral_2_eq_2 i_def)
lemma differentiable_on_open_blinfunE:
assumes "f differentiable_on S" "open S"
obtains f' where "⋀x. x ∈ S ⟹ (f has_derivative blinfun_apply (f' x)) (at x)"
proof -
{
fix x assume "x ∈ S"
with assms obtain f' where f': "(f has_derivative f') (at x)"
by (auto dest!: differentiable_on_openD simp: differentiable_def)
then have "bounded_linear f'"
by (rule has_derivative_bounded_linear)
then obtain bf' where "f' = blinfun_apply bf'"
by (metis bounded_linear_Blinfun_apply)
then have "∃bf'. (f has_derivative blinfun_apply bf') (at x)" using f'
by blast
} then obtain f' where "⋀x. x ∈ S ⟹ (f has_derivative blinfun_apply (f' x)) (at x)"
by metis
then show ?thesis ..
qed
lemma continuous_on_blinfunI1:
"continuous_on X f"
if "⋀i. i ∈ Basis ⟹ continuous_on X (λx. blinfun_apply (f x) i)"
using that
by (auto simp: continuous_on_def intro: tendsto_componentwise1)
lemma c1_euclidean_blinfunE:
fixes f::"'a::euclidean_space⇒'b::real_normed_vector"
assumes "⋀x. x ∈ S ⟹ (f has_derivative f' x) (at x within S)"
assumes "⋀i. i ∈ Basis ⟹ continuous_on S (λx. f' x i)"
obtains bf' where
"⋀x. x ∈ S ⟹ (f has_derivative blinfun_apply (bf' x)) (at x within S)"
"continuous_on S bf'"
"⋀x. x ∈ S ⟹ blinfun_apply (bf' x) = f' x"
proof -
from assms have "bounded_linear (f' x)" if "x ∈ S" for x
by (auto intro!: has_derivative_bounded_linear that)
then obtain bf' where bf': "∀x ∈ S. f' x = blinfun_apply (bf' x)"
apply atomize_elim
apply (rule bchoice)
apply auto
by (metis bounded_linear_Blinfun_apply)
with assms have "⋀x. x ∈ S ⟹ (f has_derivative blinfun_apply (bf' x)) (at x within S)"
by simp
moreover
have f_tendsto: "((λn. f' n j) ⤏ f' x j) (at x within S)"
if "x ∈ S" "j ∈ Basis"
for x j
using assms by (auto simp: continuous_on_def that)
have "continuous_on S bf'"
by (rule continuous_on_blinfunI1) (simp add: bf'[rule_format, symmetric] assms)
moreover have "⋀x. x ∈ S ⟹ blinfun_apply (bf' x) = f' x" using bf' by auto
ultimately show ?thesis ..
qed
lemma continuous_Sigma:
assumes defined: "y ∈ Pi T X"
assumes f_cont: "continuous_on (Sigma T X) (λ(t, x). f t x)"
assumes y_cont: "continuous_on T y"
shows "continuous_on T (λx. f x (y x))"
using
defined
continuous_on_compose2[OF
continuous_on_subset[where t="(λx. (x, y x)) ` T", OF f_cont]
continuous_on_Pair[OF continuous_on_id y_cont]]
by auto
lemma continuous_on_Times_swap:
"continuous_on (X × Y) (λ(x, y). f x y)"
if "continuous_on (Y × X) (λ(y, x). f x y)"
using continuous_on_compose2[OF that continuous_on_swap, where s="X × Y"]
by (auto simp: split_beta' product_swap)
lemma leibniz_rule':
"⋀x. x ∈ S ⟹
((λx. integral (cbox a b) (f x)) has_derivative (λv. integral (cbox a b) (λt. fx x t v)))
(at x within S)"
"(λx. integral (cbox a b) (f x)) differentiable_on S"
if "convex S"
and c1: "⋀t x. t ∈ cbox a b ⟹ x ∈ S ⟹ ((λx. f x t) has_derivative fx x t) (at x within S)"
"⋀i. i ∈ Basis ⟹ continuous_on (S × cbox a b) (λ(x, t). fx x t i)"
and i: "⋀x. x ∈ S ⟹ f x integrable_on cbox a b"
for S::"'a::euclidean_space set"
and f::"'a ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space"
proof -
have fx1: "continuous_on S (λx. fx x t i)" if "t ∈ cbox a b" "i ∈ Basis" for i t
by (rule continuous_Sigma[OF _ c1(2), where y="λ_. t"]) (auto simp: continuous_intros that)
{
fix x assume "x ∈ S"
have fx2: "continuous_on (cbox a b) (λt. fx x t i)" if "i ∈ Basis" for i
by (rule continuous_Sigma[OF _ continuous_on_Times_swap[OF c1(2)]])
(auto simp: continuous_intros that ‹x ∈ S›)
{
fix t
assume "t ∈ cbox a b"
have "∃f'. (∀x ∈ S. ((λx. f x t) has_derivative blinfun_apply (f' x)) (at x within S) ∧
blinfun_apply (f' x) = fx x t) ∧
continuous_on S f'"
by (rule c1_euclidean_blinfunE[OF c1(1)[OF ‹t ∈ _›] fx1[OF ‹t ∈ _›]]) (auto, metis)
} then obtain fx' where
fx':
"⋀t x. t ∈ cbox a b ⟹ x ∈ S ⟹ ((λx. f x t) has_derivative blinfun_apply (fx' t x)) (at x within S)"
"⋀t x. t ∈ cbox a b ⟹ x ∈ S ⟹ blinfun_apply (fx' t x) = fx x t"
"⋀t. t ∈ cbox a b ⟹ continuous_on S (fx' t)"
by metis
have c: "continuous_on (S × cbox a b) (λ(x, t). fx' t x)"
apply (rule continuous_on_blinfunI1)
using c1(2)
apply (rule continuous_on_eq) apply assumption
by (auto simp: fx' split_beta')
from leibniz_rule[of S a b f "λx t. fx' t x" x, OF fx'(1) i c ‹x ∈ S› ‹convex S›]
have "((λx. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (λt. fx' t x))) (at x within S)"
by auto
then have "((λx. integral (cbox a b) (f x)) has_derivative blinfun_apply (integral (cbox a b) (λt. fx' t x))) (at x within S)"
by auto
also
have fx'xi: "(λt. fx' t x) integrable_on cbox a b"
apply (rule integrable_continuous)
apply (rule continuous_on_blinfunI1)
by (simp add: fx' ‹x ∈ S› fx2)
have "blinfun_apply (integral (cbox a b) (λt. fx' t x)) = (λv. integral (cbox a b) (λxb. fx x xb v))"
apply (rule ext)
apply (subst blinfun_apply_integral)
apply (rule fx'xi)
by (simp add: ‹x ∈ S› fx' cong: integral_cong)
finally show "((λx. integral (cbox a b) (f x)) has_derivative (λc. integral (cbox a b) (λxb. fx x xb c))) (at x within S)"
by simp
} then show "(λx. integral (cbox a b) (f x)) differentiable_on S"
by (auto simp: differentiable_on_def differentiable_def)
qed
lemmas leibniz_rule'_interval = leibniz_rule'[where 'b="_::ordered_euclidean_space",
unfolded cbox_interval]
lemma leibniz_rule'_higher:
"higher_differentiable_on S (λx. integral (cbox a b) (f x)) k"
if "convex S" "open S"
and c1: "higher_differentiable_on (S×cbox a b) (λ(x, t). f x t) k"
for S::"'a::euclidean_space set"
and f::"'a ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space"
using c1
proof (induction k arbitrary: f)
case 0
then show ?case
by (auto simp: higher_differentiable_on.simps intro!: integral_continuous_on_param)
next
case (Suc k)
define D where "D x = frechet_derivative (λ(x, y). f x y) (at x)" for x
note [continuous_intros] =
Suc.prems[THEN higher_differentiable_on_imp_continuous_on, THEN continuous_on_compose2,
of _ "λx. (f x, g x)" for f g, unfolded split_beta' fst_conv snd_conv]
from Suc.prems have prems:
"⋀xt. xt ∈ S × cbox a b ⟹ (λ(x, y). f x y) differentiable at xt"
"higher_differentiable_on (S × cbox a b) (λx. D x (dx, dt)) k"
for dx dt
by (auto simp: higher_differentiable_on.simps D_def)
from frechet_derivative_worksI[OF this(1), folded D_def]
have D: "x ∈ S ⟹ t ∈ cbox a b ⟹ ((λ(x, y). f x y) has_derivative D (x, t)) (at (x, t))" for x t
by auto
have p1: "((λx. (x, t::'b)) has_derivative (λh. (h, 0))) (at x within S)" for x t
by (auto intro!: derivative_eq_intros)
have Dx: "x ∈ S ⟹ t ∈ cbox a b ⟹ ((λx. f x t) has_derivative (λdx. D (x, t) (dx, 0))) (at x within S)" for x t
by (drule has_derivative_compose[OF p1 D], assumption) auto
have cD: "continuous_on (S × cbox a b) (λ(x, t). D (x, t) v)" for v
apply (rule higher_differentiable_on_imp_continuous_on[where n=k])
using prems(2)[of "fst v" "snd v"]
by (auto simp: split_beta')
have fi: "x ∈ S ⟹ f x integrable_on cbox a b" for x
by (rule integrable_continuous) (auto intro!: continuous_intros)
from leibniz_rule'[OF ‹convex S› Dx cD fi]
have ihd: "x ∈ S ⟹ ((λx. integral (cbox a b) (f x)) has_derivative (λv. integral (cbox a b) (λt. D (x, t) (v, 0))))
(at x within S)"
and "(λx. integral (cbox a b) (f x)) differentiable_on S"
for x
by auto
then have "x ∈ S ⟹ (λx. integral (cbox a b) (f x)) differentiable at x" for x
using ‹open S›
by (auto simp: differentiable_on_openD)
moreover
have "higher_differentiable_on S (λx. frechet_derivative (λx. integral (cbox a b) (f x)) (at x) v) k" for v
proof -
have *: "frechet_derivative (λx. integral (cbox a b) (f x)) (at x) =
(λv. integral (cbox a b) (λt. D (x, t) (v, 0)))"
if "x ∈ S"
for x
apply (rule frechet_derivative_at')
using ihd(1)[OF that] at_within_open[OF that ‹open S›]
by auto
have **: "higher_differentiable_on S (λx. integral (cbox a b) (λt. D (x, t) (v, 0))) k"
apply (rule Suc.IH)
using prems by auto
show ?thesis
using ‹open S›
by (auto simp: * ** cong: higher_differentiable_on_cong)
qed
ultimately
show ?case
by (auto simp: higher_differentiable_on.simps)
qed
lemmas leibniz_rule'_higher_interval = leibniz_rule'_higher[where 'b="_::ordered_euclidean_space",
unfolded cbox_interval]
subsection ‹Smoothness›
definition k_smooth_on :: "enat ⇒'a::real_normed_vector set ⇒ ('a ⇒ 'b::real_normed_vector) ⇒ bool"
("_-smooth'_on" [1000]) where
smooth_on_def: "k-smooth_on S f = (∀n≤k. higher_differentiable_on S f n)"
abbreviation "smooth_on S f ≡ ∞-smooth_on S f"
lemma derivative_is_smooth':
assumes "(k+1)-smooth_on S f"
shows "k-smooth_on S (λx. frechet_derivative f (at x) v)"
unfolding smooth_on_def
proof (intro allI impI)
fix n assume "enat n ≤ k" then have "Suc n ≤ k + 1"
unfolding plus_1_eSuc
by (auto simp: eSuc_def split: enat.splits)
then have "higher_differentiable_on S f (Suc n)"
using assms(1) by (auto simp: smooth_on_def)
then show "higher_differentiable_on S (λx. frechet_derivative f (at x) v) n"
by (auto simp: higher_differentiable_on.simps(2))
qed
lemma derivative_is_smooth: "smooth_on S f ⟹ smooth_on S (λx. frechet_derivative f (at x) v)"
using derivative_is_smooth'[of ∞ S f] by simp
lemma smooth_on_imp_continuous_on: "continuous_on S f" if "k-smooth_on S f"
apply (rule higher_differentiable_on_imp_continuous_on[where n=0])
using that
by (simp add: smooth_on_def enat_0)
lemma smooth_on_imp_differentiable_on[simp]: "f differentiable_on S" if "k-smooth_on S f" "k ≠ 0"
using that
by (auto simp: smooth_on_def Suc_ile_eq enat_0
dest!: spec[where x=1]
intro!: higher_differentiable_on_imp_differentiable_on[where k=1])
lemma smooth_on_cong:
assumes "k-smooth_on S g" "open S"
and "⋀x. x ∈ S ⟹ f x = g x"
shows "k-smooth_on S f"
using assms unfolding smooth_on_def
by (auto cong: higher_differentiable_on_cong)
lemma smooth_on_open_Un:
"k-smooth_on S f ⟹ k-smooth_on T f ⟹ open S ⟹ open T ⟹ k-smooth_on (S ∪ T) f"
by (auto simp: smooth_on_def higher_differentiable_on_open_Un)
lemma smooth_on_open_subsetsI:
"k-smooth_on S f"
if "⋀x. x ∈ S ⟹ ∃T. x ∈ T ∧ open T ∧ k-smooth_on T f"
using that
unfolding smooth_on_def
by (force intro: higher_differentiable_on_open_subsetsI)
lemma smooth_on_const[intro]: "k-smooth_on S (λx. c)"
by (auto simp: smooth_on_def higher_differentiable_on_const)
lemma smooth_on_id[intro]: "k-smooth_on S (λx. x)"
by (auto simp: smooth_on_def higher_differentiable_on_id)
lemma smooth_on_add_fun: "k-smooth_on S f ⟹ k-smooth_on S g ⟹ open S ⟹ k-smooth_on S (f + g)"
by (auto simp: smooth_on_def higher_differentiable_on_add plus_fun_def)
lemmas smooth_on_add = smooth_on_add_fun[unfolded plus_fun_def]
lemma smooth_on_sum:
"n-smooth_on S (λx. ∑i∈F. f i x)"
if "⋀i. i ∈ F ⟹ finite F ⟹ n-smooth_on S (f i)" "open S"
using that
by (auto simp: smooth_on_def higher_differentiable_on_sum)
lemma (in bounded_bilinear) smooth_on:
includes no_matrix_mult
assumes "k-smooth_on S f" "k-smooth_on S g" "open S"
shows "k-smooth_on S (λx. (f x) ** (g x))"
using assms
by (auto simp: smooth_on_def higher_differentiable_on)
lemma smooth_on_compose2:
fixes g::"_⇒_::euclidean_space"
assumes "k-smooth_on T f" "k-smooth_on S g" "open U" "open T" "g ` U ⊆ T" "U ⊆ S"
shows "k-smooth_on U (f o g)"
using assms
by (auto simp: smooth_on_def intro!: higher_differentiable_on_compose intro: higher_differentiable_on_subset)
lemma smooth_on_compose:
fixes g::"_⇒_::euclidean_space"
assumes "k-smooth_on T f" "k-smooth_on S g" "open S" "open T" "g ` S ⊆ T"
shows "k-smooth_on S (f o g)"
using assms by (rule smooth_on_compose2) auto
lemma smooth_on_subset:
"k-smooth_on S f"
if "k-smooth_on T f" "S ⊆ T"
using higher_differentiable_on_subset[of T f _ S] that
by (auto simp: smooth_on_def)
context begin
private lemmas s = bounded_bilinear.smooth_on
lemmas smooth_on_inner = bounded_bilinear_inner[THEN s]
and smooth_on_scaleR = bounded_bilinear_scaleR[THEN s]
and smooth_on_mult = bounded_bilinear_mult[THEN s]
end
lemma smooth_on_divide:"k-smooth_on S f ⟹ k-smooth_on S g ⟹ open S ⟹(⋀x. x ∈ S ⟹ g x ≠ 0) ⟹
k-smooth_on S (λx. f x / g x)"
for f::"_⇒_::real_normed_field"
by (auto simp: smooth_on_def higher_differentiable_on_divide)
lemma smooth_on_scaleR_fun: "k-smooth_on S g ⟹ open S ⟹ k-smooth_on S (c *⇩R g)"
by (auto simp: scaleR_fun_def intro!: smooth_on_scaleR )
lemma smooth_on_uminus_fun: "k-smooth_on S g ⟹ open S ⟹ k-smooth_on S (- g)"
using smooth_on_scaleR_fun[where c="-1", of k S g]
by auto
lemmas smooth_on_uminus = smooth_on_uminus_fun[unfolded fun_Compl_def]
lemma smooth_on_minus_fun: "k-smooth_on S f ⟹ k-smooth_on S g ⟹ open S ⟹ k-smooth_on S (f - g)"
unfolding diff_conv_add_uminus
apply (rule smooth_on_add_fun)
apply assumption
apply (rule smooth_on_uminus_fun)
by auto
lemmas smooth_on_minus = smooth_on_minus_fun[unfolded fun_diff_def]
lemma smooth_on_times_fun: "k-smooth_on S f ⟹ k-smooth_on S g ⟹ open S ⟹ k-smooth_on S (f * g)"
for f g::"_ ⇒_::real_normed_algebra"
by (auto simp: times_fun_def intro!: smooth_on_mult)
lemma smooth_on_le:
"l-smooth_on S f"
if "k-smooth_on S f" "l ≤ k"
using that
by (auto simp: smooth_on_def)
lemma smooth_on_inverse: "k-smooth_on S (λx. inverse (f x))"
if "k-smooth_on S f" "0 ∉ f ` S" "open S"
for f::"_ ⇒_::real_normed_field"
using that
by (auto simp: smooth_on_def intro!: higher_differentiable_on_inverse)
lemma smooth_on_norm: "k-smooth_on S (λx. norm (f x))"
if "k-smooth_on S f" "0 ∉ f ` S" "open S"
for f::"_ ⇒_::real_inner"
using that
by (auto simp: smooth_on_def intro!: higher_differentiable_on_norm)
lemma smooth_on_sqrt: "k-smooth_on S (λx. sqrt (f x))"
if "k-smooth_on S f" "0 ∉ f ` S" "open S"
using that
by (auto simp: smooth_on_def intro!: higher_differentiable_on_sqrt)
lemma smooth_on_frechet_derivative:
"∞-smooth_on UNIV (λx. frechet_derivative f (at x) v)"
if "∞-smooth_on UNIV f"
using that
apply (auto simp: smooth_on_def)
apply (rule higher_differentiable_on_frechet_derivativeI)
by auto
lemmas smooth_on_frechet_derivivative_comp = smooth_on_compose2[OF smooth_on_frechet_derivative, unfolded o_def]
lemma smooth_onD: "higher_differentiable_on S f n" if "m-smooth_on S f" "enat n ≤ m"
using that
by (auto simp: smooth_on_def)
lemma (in bounded_linear) higher_differentiable_on: "higher_differentiable_on S f n"
proof (induction n)
case 0
then show ?case
by (auto simp: higher_differentiable_on.simps linear_continuous_on bounded_linear_axioms)
next
case (Suc n)
then show ?case
apply (auto simp: higher_differentiable_on.simps frechet_derivative higher_differentiable_on_const)
using bounded_linear_axioms apply (rule bounded_linear_imp_differentiable)
done
qed
lemma (in bounded_linear) smooth_on: "k-smooth_on S f"
by (auto simp: smooth_on_def higher_differentiable_on)
lemma smooth_on_snd:
"k-smooth_on S (λx. snd (f x))"
if "k-smooth_on S f" "open S"
using higher_differentiable_on_snd_comp that
by (auto simp: smooth_on_def)
lemma smooth_on_fst:
"k-smooth_on S (λx. fst (f x))"
if "k-smooth_on S f" "open S"
using higher_differentiable_on_fst_comp that
by (auto simp: smooth_on_def)
lemma smooth_on_sin: "n-smooth_on S (λx. sin (f x::real))" if "n-smooth_on S f" "open S"
using that
by (auto simp: smooth_on_def intro!: higher_differentiable_on_sin)
lemma smooth_on_cos: "n-smooth_on S (λx. cos (f x::real))" if "n-smooth_on S f" "open S"
using that
by (auto simp: smooth_on_def intro!: higher_differentiable_on_cos)
lemma smooth_on_Taylor2E:
fixes f::"'a::euclidean_space ⇒ real"
assumes hd: "∞-smooth_on UNIV f"
obtains g where "⋀Y.
f Y = f X + frechet_derivative f (at X) (Y - X) + (∑i∈Basis. (∑j∈Basis. ((Y - X) ∙ j) * ((Y - X) ∙ i) * g i j Y))"
"⋀i j. i ∈ Basis ⟹ j ∈ Basis ⟹ ∞-smooth_on UNIV (g i j)"
proof -
define S::"'a set" where "S = UNIV"
have "open S" and "convex S" "X ∈ S" by (auto simp: S_def)
have hd: "∞-smooth_on S f"
using hd by (auto simp: S_def)
define i where "i H x = ((1 - x)) *⇩R nth_derivative 2 f (X + x *⇩R H) H" for x H
define d2 where "d2 v v' = (λx. frechet_derivative (λx. frechet_derivative f (at x) v') (at x) v)" for v v'
define g where "g H x i j = d2 i j (X + x *⇩R H)" for i j x H
define g' where "g' i j H = integral {0 .. 1} (λx. (1 - x) * g H x i j)" for i j H
have "higher_differentiable_on S f 2"
using hd(1) by (auto simp: smooth_on_def dest!: spec[where x=2])
note hd2 = this ‹open S›
have d2_cont: "continuous_on S (d2 i j)" for i j
using hd2(1)
by (auto simp: g_def numeral_2_eq_2 higher_differentiable_on.simps d2_def)
note [continuous_intros] = continuous_on_compose2[OF d2_cont]
have hdiff2: "∞-smooth_on S (d2 v v')" for v v'
apply (auto simp: d2_def)
apply (rule smooth_on_frechet_derivivative_comp)
apply (rule smooth_on_frechet_derivivative_comp)
by (auto simp: S_def assms)
{
fix Y
assume "Y ∈ S"
define H where "H = Y - X"
from ‹Y ∈ S› have "X + H ∈ S" by (simp add: H_def)
with ‹X ∈ S› have cs: "closed_segment X (X + H) ⊆ S"
using ‹convex S›
by (rule closed_segment_subset)
have i: "(i H has_integral f (X + H) - (f X + nth_derivative 1 f X H)) {0..1}"
"f (X + H) = f X + nth_derivative 1 f X H + integral {0..1} (i H)"
"i H integrable_on {0..1}"
unfolding i_def
using higher_differentiable_Taylor1[OF hd2 cs]
by auto
note i(2)
also
have integrable: "(λx. ∑n∈Basis. (1 - x) * (g H x a n * (H ∙ n) * (H ∙ a))) integrable_on {0..1}"
"(λx. (1 - x) * (g H x n a * (H ∙ a) * (H ∙ n))) integrable_on {0..1}"
for a n
by (auto intro!: integrable_continuous_interval continuous_intros closed_segment_subsetD
cs simp: g_def)
have i_eq: "i H x = (1 - x) *⇩R (∑i∈Basis. (∑j∈Basis. g H x i j * (H ∙ j)) * (H ∙ i))"
if "0 ≤ x" "x ≤ 1"
for x
unfolding i_def
apply (subst second_derivative_componentwise[OF hd2])
apply (rule closed_segment_subsetD, rule cs, rule that, rule that)
by (simp add: g_def d2_def)
have "integral {0 .. 1} (i H) = integral {0..1} (λx. (1 - x) * (∑i∈Basis. (∑j∈Basis. g H x i j * (H ∙ j)) * (H ∙ i)))"
apply (subst integral_spike[OF negligible_empty])
apply (rule sym)
apply (rule i_eq)
by (auto simp: that)
also
have "… = (∑i∈Basis. (∑j∈Basis. (H ∙ j) * (H ∙ i) * g' i j H))"
apply (simp add: sum_distrib_left sum_distrib_right integral_sum integrable g'_def)
apply (simp add: integral_mult_right[symmetric] del: integral_mult_right)
by (simp only: ac_simps)
finally have "f (X + H) = f X + nth_derivative 1 f X H + (∑i∈Basis. ∑j∈Basis. H ∙ j * (H ∙ i) * g' i j H)" .
} note * = this
have "f Y = f X + frechet_derivative f (at X) (Y - X) + (∑i∈Basis. ∑j∈Basis. (Y - X) ∙ j * ((Y - X) ∙ i) * g' i j (Y - X))"
for Y
using *[of Y]
by (auto simp: S_def)
moreover
define T::"real set" where "T = {- 1<..<2}"
have "open T"
by (auto simp: T_def)
have "{0 .. 1} ⊆ T"
by (auto simp: T_def)
have T_small: "a ∈ S ⟹ b ∈ T ⟹ X + b *⇩R (a - X) ∈ S" for a b
by (auto simp: S_def)
have "open (S × T)"
by (auto intro: open_Times ‹open S› ‹open T›)
have "smooth_on S (λY. g' i j (Y - X))" if i: "i ∈ Basis" and j: "j ∈ Basis" for i j
unfolding smooth_on_def
apply safe
apply (simp add: g'_def)
apply (rule leibniz_rule'_higher_interval)
apply fact
apply fact
apply (rule higher_differentiable_on_subset[where T="S × T"])
apply (auto intro!: higher_differentiable_on_mult simp: split_beta')
apply (subst diff_conv_add_uminus)
apply (rule higher_differentiable_on_add)
apply (rule higher_differentiable_on_const)
apply (subst scaleR_minus1_left[symmetric])
apply (rule higher_differentiable_on_scaleR)
apply (rule higher_differentiable_on_const)
apply (rule higher_differentiable_on_snd_comp)
apply (rule higher_differentiable_on_id)
apply fact apply fact apply fact
apply (auto simp: g_def)
apply (rule smooth_onD)
apply (rule smooth_on_compose2[OF hdiff2, unfolded o_def])
using ‹open S› ‹open T›
using T_small ‹_ ⊆ T›
by (auto intro!: open_Times smooth_on_add smooth_on_scaleR smooth_on_snd
smooth_on_minus smooth_on_fst)
ultimately show ?thesis unfolding S_def ..
qed
lemma smooth_on_Pair:
"k-smooth_on S (λx. (f x, g x))"
if "open S" "k-smooth_on S f" "k-smooth_on S g"
proof (auto simp: smooth_on_def)
fix n assume n: "enat n ≤ k"
have 1: "higher_differentiable_on S f n"
using that(2) n unfolding smooth_on_def by auto
have 2: "higher_differentiable_on S g n"
using that(3) n unfolding smooth_on_def by auto
show "higher_differentiable_on S (λx. (f x, g x)) n"
by (rule higher_differentiable_on_Pair [OF that(1) 1 2])
qed
lemma smooth_on_Pair':
"k-smooth_on (S × T) (λx. (f (fst x), g (snd x)))"
if "open S" "open T" "k-smooth_on S f" "k-smooth_on T g"
for f::"_::euclidean_space⇒_" and g::"_::euclidean_space⇒_"
proof (auto simp: smooth_on_def)
fix n assume n: "enat n ≤ k"
have 1: "higher_differentiable_on S f n"
using that(3) n unfolding smooth_on_def by auto
have 2: "higher_differentiable_on T g n"
using that(4) n unfolding smooth_on_def by auto
show "higher_differentiable_on (S × T) (λx. (f (fst x), g (snd x))) n"
by (rule higher_differentiable_on_Pair'[OF that(1,2) 1 2])
qed
subsection ‹Diffeomorphism›
definition "diffeomorphism k S T p p' ⟷
k-smooth_on S p ∧ k-smooth_on T p' ∧ homeomorphism S T p p'"
lemma diffeomorphism_imp_homeomorphism:
assumes "diffeomorphism k s t p p'"
shows "homeomorphism s t p p'"
using assms
by (auto simp: diffeomorphism_def)
lemma diffeomorphismD:
assumes "diffeomorphism k S T f g"
shows diffeomorphism_smoothD: "k-smooth_on S f" "k-smooth_on T g"
and diffeomorphism_inverseD: "⋀x. x ∈ S ⟹ g (f x) = x" "⋀y. y ∈ T ⟹ f (g y) = y"
and diffeomorphism_image_eq: "(f ` S = T)" "(g ` T = S)"
using assms by (auto simp: diffeomorphism_def homeomorphism_def)
lemma diffeomorphism_compose:
"diffeomorphism n S T f g ⟹ diffeomorphism n T U h k ⟹ open S ⟹ open T ⟹ open U ⟹
diffeomorphism n S U (h ∘ f) (g ∘ k)"
for f::"_⇒_::euclidean_space"
by (auto simp: diffeomorphism_def intro!: smooth_on_compose homeomorphism_compose)
(auto simp: homeomorphism_def)
lemma diffeomorphism_add: "diffeomorphism k UNIV UNIV (λx. x + c) (λx. x - c)"
by (auto simp: diffeomorphism_def homeomorphism_add intro!: smooth_on_minus smooth_on_add)
lemma diffeomorphism_scaleR: "diffeomorphism k UNIV UNIV (λx. c *⇩R x) (λx. x /⇩R c)"
if "c ≠ 0"
by (auto simp: that diffeomorphism_def homeomorphism_scaleR
intro!: smooth_on_minus smooth_on_scaleR)
end