mathlib3 documentation

analysis.calculus.fderiv.comp

The derivative of a composition (chain rule) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For detailed documentation of the Fréchet derivative, see the module docstring of analysis/calculus/fderiv/basic.lean.

This file contains the usual formulas (and existence assertions) for the derivative of composition of functions (the chain rule).

Derivative of the composition of two functions #

For composition lemmas, we put x explicit to help the elaborator, as otherwise Lean tends to get confused since there are too many possibilities for composition

theorem has_fderiv_at_filter.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {f' : E →L[𝕜] F} (x : E) {L : filter E} {g : F G} {g' : F →L[𝕜] G} {L' : filter F} (hg : has_fderiv_at_filter g g' (f x) L') (hf : has_fderiv_at_filter f f' x L) (hL : filter.tendsto f L L') :
has_fderiv_at_filter (g f) (g'.comp f') x L
theorem has_fderiv_within_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {f' : E →L[𝕜] F} (x : E) {s : set E} {g : F G} {g' : F →L[𝕜] G} {t : set F} (hg : has_fderiv_within_at g g' t (f x)) (hf : has_fderiv_within_at f f' s x) (hst : set.maps_to f s t) :
has_fderiv_within_at (g f) (g'.comp f') s x
theorem has_fderiv_at.comp_has_fderiv_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {f' : E →L[𝕜] F} (x : E) {s : set E} {g : F G} {g' : F →L[𝕜] G} (hg : has_fderiv_at g g' (f x)) (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (g f) (g'.comp f') s x
theorem has_fderiv_within_at.comp_of_mem {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {f' : E →L[𝕜] F} (x : E) {s : set E} {g : F G} {g' : F →L[𝕜] G} {t : set F} (hg : has_fderiv_within_at g g' t (f x)) (hf : has_fderiv_within_at f f' s x) (hst : filter.tendsto f (nhds_within x s) (nhds_within (f x) t)) :
has_fderiv_within_at (g f) (g'.comp f') s x
theorem has_fderiv_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {f' : E →L[𝕜] F} (x : E) {g : F G} {g' : F →L[𝕜] G} (hg : has_fderiv_at g g' (f x)) (hf : has_fderiv_at f f' x) :
has_fderiv_at (g f) (g'.comp f') x

The chain rule.

theorem differentiable_within_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} (x : E) {s : set E} {g : F G} {t : set F} (hg : differentiable_within_at 𝕜 g t (f x)) (hf : differentiable_within_at 𝕜 f s x) (h : set.maps_to f s t) :
theorem differentiable_within_at.comp' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} (x : E) {s : set E} {g : F G} {t : set F} (hg : differentiable_within_at 𝕜 g t (f x)) (hf : differentiable_within_at 𝕜 f s x) :
differentiable_within_at 𝕜 (g f) (s f ⁻¹' t) x
theorem differentiable_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} (x : E) {g : F G} (hg : differentiable_at 𝕜 g (f x)) (hf : differentiable_at 𝕜 f x) :
differentiable_at 𝕜 (g f) x
theorem differentiable_at.comp_differentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} (x : E) {s : set E} {g : F G} (hg : differentiable_at 𝕜 g (f x)) (hf : differentiable_within_at 𝕜 f s x) :
theorem fderiv_within.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} (x : E) {s : set E} {g : F G} {t : set F} (hg : differentiable_within_at 𝕜 g t (f x)) (hf : differentiable_within_at 𝕜 f s x) (h : set.maps_to f s t) (hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (g f) s x = (fderiv_within 𝕜 g t (f x)).comp (fderiv_within 𝕜 f s x)
theorem fderiv_within_fderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {g : F G} {f : E F} {x : E} {y : F} {s : set E} {t : set F} (hg : differentiable_within_at 𝕜 g t y) (hf : differentiable_within_at 𝕜 f s x) (h : set.maps_to f s t) (hxs : unique_diff_within_at 𝕜 s x) (hy : f x = y) (v : E) :
(fderiv_within 𝕜 g t y) ((fderiv_within 𝕜 f s x) v) = (fderiv_within 𝕜 (g f) s x) v

A version of fderiv_within.comp that is useful to rewrite the composition of two derivatives into a single derivative. This version always applies, but creates a new side-goal f x = y.

theorem fderiv_within.comp₃ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {G' : Type u_5} [normed_add_comm_group G'] [normed_space 𝕜 G'] {f : E F} (x : E) {s : set E} {g' : G G'} {g : F G} {t : set F} {u : set G} {y : F} {y' : G} (hg' : differentiable_within_at 𝕜 g' u y') (hg : differentiable_within_at 𝕜 g t y) (hf : differentiable_within_at 𝕜 f s x) (h2g : set.maps_to g t u) (h2f : set.maps_to f s t) (h3g : g y = y') (h3f : f x = y) (hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (g' g f) s x = (fderiv_within 𝕜 g' u y').comp ((fderiv_within 𝕜 g t y).comp (fderiv_within 𝕜 f s x))

Ternary version of fderiv_within.comp, with equality assumptions of basepoints added, in order to apply more easily as a rewrite from right-to-left.

theorem fderiv.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} (x : E) {g : F G} (hg : differentiable_at 𝕜 g (f x)) (hf : differentiable_at 𝕜 f x) :
fderiv 𝕜 (g f) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x)
theorem fderiv.comp_fderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} (x : E) {s : set E} {g : F G} (hg : differentiable_at 𝕜 g (f x)) (hf : differentiable_within_at 𝕜 f s x) (hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (g f) s x = (fderiv 𝕜 g (f x)).comp (fderiv_within 𝕜 f s x)
theorem differentiable_on.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {s : set E} {g : F G} {t : set F} (hg : differentiable_on 𝕜 g t) (hf : differentiable_on 𝕜 f s) (st : set.maps_to f s t) :
differentiable_on 𝕜 (g f) s
theorem differentiable.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {g : F G} (hg : differentiable 𝕜 g) (hf : differentiable 𝕜 f) :
differentiable 𝕜 (g f)
theorem differentiable.comp_differentiable_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {s : set E} {g : F G} (hg : differentiable 𝕜 g) (hf : differentiable_on 𝕜 f s) :
differentiable_on 𝕜 (g f) s
@[protected]
theorem has_strict_fderiv_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {f' : E →L[𝕜] F} (x : E) {g : F G} {g' : F →L[𝕜] G} (hg : has_strict_fderiv_at g g' (f x)) (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), g (f x)) (g'.comp f') x

The chain rule for derivatives in the sense of strict differentiability.

@[protected]
theorem differentiable.iterate {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {f : E E} (hf : differentiable 𝕜 f) (n : ) :
@[protected]
theorem differentiable_on.iterate {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {f : E E} (hf : differentiable_on 𝕜 f s) (hs : set.maps_to f s s) (n : ) :
@[protected]
theorem has_fderiv_at_filter.iterate {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {L : filter E} {f : E E} {f' : E →L[𝕜] E} (hf : has_fderiv_at_filter f f' x L) (hL : filter.tendsto f L L) (hx : f x = x) (n : ) :
@[protected]
theorem has_fderiv_at.iterate {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {f : E E} {f' : E →L[𝕜] E} (hf : has_fderiv_at f f' x) (hx : f x = x) (n : ) :
has_fderiv_at f^[n] (f' ^ n) x
@[protected]
theorem has_fderiv_within_at.iterate {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s : set E} {f : E E} {f' : E →L[𝕜] E} (hf : has_fderiv_within_at f f' s x) (hx : f x = x) (hs : set.maps_to f s s) (n : ) :
@[protected]
theorem has_strict_fderiv_at.iterate {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {f : E E} {f' : E →L[𝕜] E} (hf : has_strict_fderiv_at f f' x) (hx : f x = x) (n : ) :
@[protected]
theorem differentiable_at.iterate {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {f : E E} (hf : differentiable_at 𝕜 f x) (hx : f x = x) (n : ) :
@[protected]
theorem differentiable_within_at.iterate {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {s : set E} {f : E E} (hf : differentiable_within_at 𝕜 f s x) (hx : f x = x) (hs : set.maps_to f s s) (n : ) :