Derivative of the cartesian product of functions #

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 cartesian products of functions, and functions into Pi-types.

Derivative of the cartesian product of two functions #

source

theorem HasStrictFDerivAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {f₂ : E → G} {f₂' : E →L[𝕜] G} (hf₁ : HasStrictFDerivAt f₁ f₁' x) (hf₂ : HasStrictFDerivAt f₂ f₂' x) :

HasStrictFDerivAt (fun (x : E) => (f₁ x, f₂ x)) (ContinuousLinearMap.prod f₁' f₂') x

source

theorem HasFDerivAtFilter.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {L : Filter E} {f₂ : E → G} {f₂' : E →L[𝕜] G} (hf₁ : HasFDerivAtFilter f₁ f₁' x L) (hf₂ : HasFDerivAtFilter f₂ f₂' x L) :

HasFDerivAtFilter (fun (x : E) => (f₁ x, f₂ x)) (ContinuousLinearMap.prod f₁' f₂') x L

source

theorem HasFDerivWithinAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {s : Set E} {f₂ : E → G} {f₂' : E →L[𝕜] G} (hf₁ : HasFDerivWithinAt f₁ f₁' s x) (hf₂ : HasFDerivWithinAt f₂ f₂' s x) :

HasFDerivWithinAt (fun (x : E) => (f₁ x, f₂ x)) (ContinuousLinearMap.prod f₁' f₂') s x

source

theorem HasFDerivAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {f₁' : E →L[𝕜] F} {x : E} {f₂ : E → G} {f₂' : E →L[𝕜] G} (hf₁ : HasFDerivAt f₁ f₁' x) (hf₂ : HasFDerivAt f₂ f₂' x) :

HasFDerivAt (fun (x : E) => (f₁ x, f₂ x)) (ContinuousLinearMap.prod f₁' f₂') x

source

theorem hasFDerivAt_prod_mk_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e₀ : E) (f₀ : F) :

HasFDerivAt (fun (e : E) => (e, f₀)) (ContinuousLinearMap.inl 𝕜 E F) e₀

source

theorem hasFDerivAt_prod_mk_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e₀ : E) (f₀ : F) :

HasFDerivAt (fun (f : F) => (e₀, f)) (ContinuousLinearMap.inr 𝕜 E F) f₀

source

theorem DifferentiableWithinAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {s : Set E} {f₂ : E → G} (hf₁ : DifferentiableWithinAt 𝕜 f₁ s x) (hf₂ : DifferentiableWithinAt 𝕜 f₂ s x) :

DifferentiableWithinAt 𝕜 (fun (x : E) => (f₁ x, f₂ x)) s x

source

@[simp]

theorem DifferentiableAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {f₂ : E → G} (hf₁ : DifferentiableAt 𝕜 f₁ x) (hf₂ : DifferentiableAt 𝕜 f₂ x) :

DifferentiableAt 𝕜 (fun (x : E) => (f₁ x, f₂ x)) x

source

theorem DifferentiableOn.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {s : Set E} {f₂ : E → G} (hf₁ : DifferentiableOn 𝕜 f₁ s) (hf₂ : DifferentiableOn 𝕜 f₂ s) :

DifferentiableOn 𝕜 (fun (x : E) => (f₁ x, f₂ x)) s

source

@[simp]

theorem Differentiable.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {f₂ : E → G} (hf₁ : Differentiable 𝕜 f₁) (hf₂ : Differentiable 𝕜 f₂) :

Differentiable 𝕜 fun (x : E) => (f₁ x, f₂ x)

source

theorem DifferentiableAt.fderiv_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {f₂ : E → G} (hf₁ : DifferentiableAt 𝕜 f₁ x) (hf₂ : DifferentiableAt 𝕜 f₂ x) :

fderiv 𝕜 (fun (x : E) => (f₁ x, f₂ x)) x = ContinuousLinearMap.prod (fderiv 𝕜 f₁ x) (fderiv 𝕜 f₂ x)

source

theorem DifferentiableWithinAt.fderivWithin_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₁ : E → F} {x : E} {s : Set E} {f₂ : E → G} (hf₁ : DifferentiableWithinAt 𝕜 f₁ s x) (hf₂ : DifferentiableWithinAt 𝕜 f₂ s x) (hxs : UniqueDiffWithinAt 𝕜 s x) :

fderivWithin 𝕜 (fun (x : E) => (f₁ x, f₂ x)) s x = ContinuousLinearMap.prod (fderivWithin 𝕜 f₁ s x) (fderivWithin 𝕜 f₂ s x)

source

theorem hasStrictFDerivAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

HasStrictFDerivAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p

source

theorem HasStrictFDerivAt.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasStrictFDerivAt f₂ f₂' x) :

HasStrictFDerivAt (fun (x : E) => (f₂ x).1) (ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) f₂') x

source

theorem hasFDerivAtFilter_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {L : Filter (E × F)} :

HasFDerivAtFilter Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p L

source

theorem HasFDerivAtFilter.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {L : Filter E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivAtFilter f₂ f₂' x L) :

HasFDerivAtFilter (fun (x : E) => (f₂ x).1) (ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) f₂') x L

source

theorem hasFDerivAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

HasFDerivAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p

source

theorem HasFDerivAt.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivAt f₂ f₂' x) :

HasFDerivAt (fun (x : E) => (f₂ x).1) (ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) f₂') x

source

theorem hasFDerivWithinAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} :

HasFDerivWithinAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) s p

source

theorem HasFDerivWithinAt.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivWithinAt f₂ f₂' s x) :

HasFDerivWithinAt (fun (x : E) => (f₂ x).1) (ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) f₂') s x

source

theorem differentiableAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

DifferentiableAt 𝕜 Prod.fst p

source

@[simp]

theorem DifferentiableAt.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} (h : DifferentiableAt 𝕜 f₂ x) :

DifferentiableAt 𝕜 (fun (x : E) => (f₂ x).1) x

source

theorem differentiable_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :

Differentiable 𝕜 Prod.fst

source

@[simp]

theorem Differentiable.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₂ : E → F × G} (h : Differentiable 𝕜 f₂) :

Differentiable 𝕜 fun (x : E) => (f₂ x).1

source

theorem differentiableWithinAt_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} :

DifferentiableWithinAt 𝕜 Prod.fst s p

source

theorem DifferentiableWithinAt.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G} (h : DifferentiableWithinAt 𝕜 f₂ s x) :

DifferentiableWithinAt 𝕜 (fun (x : E) => (f₂ x).1) s x

source

theorem differentiableOn_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set (E × F)} :

DifferentiableOn 𝕜 Prod.fst s

source

theorem DifferentiableOn.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f₂ : E → F × G} (h : DifferentiableOn 𝕜 f₂ s) :

DifferentiableOn 𝕜 (fun (x : E) => (f₂ x).1) s

source

theorem fderiv_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

fderiv 𝕜 Prod.fst p = ContinuousLinearMap.fst 𝕜 E F

source

theorem fderiv.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} (h : DifferentiableAt 𝕜 f₂ x) :

fderiv 𝕜 (fun (x : E) => (f₂ x).1) x = ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) (fderiv 𝕜 f₂ x)

source

theorem fderivWithin_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} (hs : UniqueDiffWithinAt 𝕜 s p) :

fderivWithin 𝕜 Prod.fst s p = ContinuousLinearMap.fst 𝕜 E F

source

theorem fderivWithin.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G} (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f₂ s x) :

fderivWithin 𝕜 (fun (x : E) => (f₂ x).1) s x = ContinuousLinearMap.comp (ContinuousLinearMap.fst 𝕜 F G) (fderivWithin 𝕜 f₂ s x)

source

theorem hasStrictFDerivAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

HasStrictFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p

source

theorem HasStrictFDerivAt.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasStrictFDerivAt f₂ f₂' x) :

HasStrictFDerivAt (fun (x : E) => (f₂ x).2) (ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) f₂') x

source

theorem hasFDerivAtFilter_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {L : Filter (E × F)} :

HasFDerivAtFilter Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p L

source

theorem HasFDerivAtFilter.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {L : Filter E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivAtFilter f₂ f₂' x L) :

HasFDerivAtFilter (fun (x : E) => (f₂ x).2) (ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) f₂') x L

source

theorem hasFDerivAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

HasFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p

source

theorem HasFDerivAt.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivAt f₂ f₂' x) :

HasFDerivAt (fun (x : E) => (f₂ x).2) (ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) f₂') x

source

theorem hasFDerivWithinAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} :

HasFDerivWithinAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) s p

source

theorem HasFDerivWithinAt.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} (h : HasFDerivWithinAt f₂ f₂' s x) :

HasFDerivWithinAt (fun (x : E) => (f₂ x).2) (ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) f₂') s x

source

theorem differentiableAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

DifferentiableAt 𝕜 Prod.snd p

source

@[simp]

theorem DifferentiableAt.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} (h : DifferentiableAt 𝕜 f₂ x) :

DifferentiableAt 𝕜 (fun (x : E) => (f₂ x).2) x

source

theorem differentiable_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :

Differentiable 𝕜 Prod.snd

source

@[simp]

theorem Differentiable.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₂ : E → F × G} (h : Differentiable 𝕜 f₂) :

Differentiable 𝕜 fun (x : E) => (f₂ x).2

source

theorem differentiableWithinAt_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} :

DifferentiableWithinAt 𝕜 Prod.snd s p

source

theorem DifferentiableWithinAt.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G} (h : DifferentiableWithinAt 𝕜 f₂ s x) :

DifferentiableWithinAt 𝕜 (fun (x : E) => (f₂ x).2) s x

source

theorem differentiableOn_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set (E × F)} :

DifferentiableOn 𝕜 Prod.snd s

source

theorem DifferentiableOn.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f₂ : E → F × G} (h : DifferentiableOn 𝕜 f₂ s) :

DifferentiableOn 𝕜 (fun (x : E) => (f₂ x).2) s

source

theorem fderiv_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} :

fderiv 𝕜 Prod.snd p = ContinuousLinearMap.snd 𝕜 E F

source

theorem fderiv.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} (h : DifferentiableAt 𝕜 f₂ x) :

fderiv 𝕜 (fun (x : E) => (f₂ x).2) x = ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) (fderiv 𝕜 f₂ x)

source

theorem fderivWithin_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : E × F} {s : Set (E × F)} (hs : UniqueDiffWithinAt 𝕜 s p) :

fderivWithin 𝕜 Prod.snd s p = ContinuousLinearMap.snd 𝕜 E F

source

theorem fderivWithin.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {f₂ : E → F × G} (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f₂ s x) :

fderivWithin 𝕜 (fun (x : E) => (f₂ x).2) s x = ContinuousLinearMap.comp (ContinuousLinearMap.snd 𝕜 F G) (fderivWithin 𝕜 f₂ s x)

source

theorem HasStrictFDerivAt.prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {f : E → F} {f' : E →L[𝕜] F} {f₂ : G → G'} {f₂' : G →L[𝕜] G'} (p : E × G) (hf : HasStrictFDerivAt f f' p.1) (hf₂ : HasStrictFDerivAt f₂ f₂' p.2) :

HasStrictFDerivAt (Prod.map f f₂) (ContinuousLinearMap.prodMap f' f₂') p

source

theorem HasFDerivAt.prodMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {f : E → F} {f' : E →L[𝕜] F} {f₂ : G → G'} {f₂' : G →L[𝕜] G'} (p : E × G) (hf : HasFDerivAt f f' p.1) (hf₂ : HasFDerivAt f₂ f₂' p.2) :

HasFDerivAt (Prod.map f f₂) (ContinuousLinearMap.prodMap f' f₂') p

source

@[simp]

theorem DifferentiableAt.prod_map {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] {f : E → F} {f₂ : G → G'} (p : E × G) (hf : DifferentiableAt 𝕜 f p.1) (hf₂ : DifferentiableAt 𝕜 f₂ p.2) :

DifferentiableAt 𝕜 (fun (p : E × G) => (f p.1, f₂ p.2)) p

Derivatives of functions `f : E → Π i, F' i` #

In this section we formulate has*FDeriv*_pi theorems as iffs, and provide two versions of each theorem:

the version without ' deals with φ : Π i, E → F' i and φ' : Π i, E →L[𝕜] F' i and is designed to deduce differentiability of fun x i ↦ φ i x from differentiability of each φ i;
the version with ' deals with Φ : E → Π i, F' i and Φ' : E →L[𝕜] Π i, F' i and is designed to deduce differentiability of the components fun x ↦ Φ x i from differentiability of Φ.

source

@[simp]

theorem hasStrictFDerivAt_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} :

HasStrictFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') x

source

@[simp]

theorem hasStrictFDerivAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i} :

HasStrictFDerivAt (fun (x : E) (i : ι) => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ (i : ι), HasStrictFDerivAt (φ i) (φ' i) x

source

@[simp]

theorem hasFDerivAtFilter_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {L : Filter E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} :

HasFDerivAtFilter Φ Φ' x L ↔ ∀ (i : ι), HasFDerivAtFilter (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') x L

source

theorem hasFDerivAtFilter_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {L : Filter E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i} :

HasFDerivAtFilter (fun (x : E) (i : ι) => φ i x) (ContinuousLinearMap.pi φ') x L ↔ ∀ (i : ι), HasFDerivAtFilter (φ i) (φ' i) x L

source

@[simp]

theorem hasFDerivAt_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} :

HasFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasFDerivAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') x

source

theorem hasFDerivAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i} :

HasFDerivAt (fun (x : E) (i : ι) => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ (i : ι), HasFDerivAt (φ i) (φ' i) x

source

@[simp]

theorem hasFDerivWithinAt_pi' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} :

HasFDerivWithinAt Φ Φ' s x ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : E) => Φ x i) (ContinuousLinearMap.comp (ContinuousLinearMap.proj i) Φ') s x

source

theorem hasFDerivWithinAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} {φ' : (i : ι) → E →L[𝕜] F' i} :

HasFDerivWithinAt (fun (x : E) (i : ι) => φ i x) (ContinuousLinearMap.pi φ') s x ↔ ∀ (i : ι), HasFDerivWithinAt (φ i) (φ' i) s x

source

@[simp]

theorem differentiableWithinAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} :

DifferentiableWithinAt 𝕜 Φ s x ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun (x : E) => Φ x i) s x

source

@[simp]

theorem differentiableAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} :

DifferentiableAt 𝕜 Φ x ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun (x : E) => Φ x i) x

source

theorem differentiableOn_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} :

DifferentiableOn 𝕜 Φ s ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun (x : E) => Φ x i) s

source

theorem differentiable_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i} :

Differentiable 𝕜 Φ ↔ ∀ (i : ι), Differentiable 𝕜 fun (x : E) => Φ x i

source

theorem fderivWithin_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} (h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (φ i) s x) (hs : UniqueDiffWithinAt 𝕜 s x) :

fderivWithin 𝕜 (fun (x : E) (i : ι) => φ i x) s x = ContinuousLinearMap.pi fun (i : ι) => fderivWithin 𝕜 (φ i) s x

source

theorem fderiv_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i} (h : ∀ (i : ι), DifferentiableAt 𝕜 (φ i) x) :

fderiv 𝕜 (fun (x : E) (i : ι) => φ i x) x = ContinuousLinearMap.pi fun (i : ι) => fderiv 𝕜 (φ i) x

Documentation

Mathlib.Analysis.Calculus.FDeriv.Prod

Derivative of the cartesian product of functions #

Derivative of the cartesian product of two functions #

Derivatives of functions `f : E → Π i, F' i` #

Derivative of the cartesian product of functions #

Derivative of the cartesian product of two functions #

Derivatives of functions f : E → Π i, F' i #

Derivatives of functions `f : E → Π i, F' i` #