# 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.prodMk {𝕜 : 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)) (f₁'.prod f₂') x
source
theorem HasFDerivAtFilter.prodMk {𝕜 : 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)) (f₁'.prod f₂') x L
source
theorem HasFDerivWithinAt.prodMk {𝕜 : 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)) (f₁'.prod f₂') s x
source
theorem HasFDerivAt.prodMk {𝕜 : 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)) (f₁'.prod f₂') x
source
theorem hasFDerivAt_prodMk_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_prodMk_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.prodMk {𝕜 : 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.prodMk {𝕜 : 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.prodMk {𝕜 : 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.prodMk {𝕜 : 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_prodMk {𝕜 : 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 = (fderiv 𝕜 f₁ x).prod (fderiv 𝕜 f₂ x)
source
theorem DifferentiableWithinAt.fderivWithin_prodMk {𝕜 : 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 = (fderivWithin 𝕜 f₁ s x).prod (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.fst 𝕜 F G).comp 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.fst 𝕜 F G).comp 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.fst 𝕜 F G).comp 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.fst 𝕜 F G).comp 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.fst 𝕜 F G).comp (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.fst 𝕜 F G).comp (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.snd 𝕜 F G).comp 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.snd 𝕜 F G).comp 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.snd 𝕜 F G).comp 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.snd 𝕜 F G).comp 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.snd 𝕜 F G).comp (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.snd 𝕜 F G).comp (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₂) (f'.prodMap f₂') p
source
theorem HasFDerivWithinAt.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) {s : Set (E × G)} (hf : HasFDerivWithinAt f f' (Prod.fst '' s) p.1) (hf₂ : HasFDerivWithinAt f₂ f₂' (Prod.snd '' s) p.2) :
HasFDerivWithinAt (Prod.map f f₂) (f'.prodMap f₂') s 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₂) (f'.prodMap f₂') p
source
@[simp]
theorem DifferentiableAt.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₂ : 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 `iff`s, 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.proj i).comp Φ') x
source
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} (hφ : ∀ (i : ι), HasStrictFDerivAt (fun (x : E) => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') x) :
HasStrictFDerivAt Φ Φ' x
source
theorem hasStrictFDerivAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) :
HasStrictFDerivAt (fun (f : (i : ι) → F' i) => f i) (ContinuousLinearMap.proj i) f
source
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.proj i).comp Φ') 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.proj i).comp Φ') 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)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} (hφ : ∀ (i : ι), HasFDerivAt (fun (x : E) => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') x) :
HasFDerivAt Φ Φ' x
source
theorem hasFDerivAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) :
HasFDerivAt (fun (f : (i : ι) → F' i) => f i) (ContinuousLinearMap.proj i) f
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.proj i).comp Φ') 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)] {Φ : E → (i : ι) → F' i} {Φ' : E →L[𝕜] (i : ι) → F' i} (hφ : ∀ (i : ι), HasFDerivWithinAt (fun (x : E) => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') s x) :
HasFDerivWithinAt Φ Φ' s x
source
theorem hasFDerivWithinAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) (s' : Set ((i : ι) → F' i)) :
HasFDerivWithinAt (fun (f : (i : ι) → F' i) => f i) (ContinuousLinearMap.proj i) s' f
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
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} (hφ : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun (x : E) => Φ x i) s x) :
DifferentiableWithinAt 𝕜 Φ s x
source
theorem differentiableWithinAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) (s' : Set ((i : ι) → F' i)) :
DifferentiableWithinAt 𝕜 (fun (f : (i : ι) → F' i) => f i) s' f
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 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} (hφ : ∀ (i : ι), DifferentiableAt 𝕜 (fun (x : E) => Φ x i) x) :
DifferentiableAt 𝕜 Φ x
source
theorem differentiableAt_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i) :
DifferentiableAt 𝕜 (fun (f : (i : ι) → F' i) => f i) f
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 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} (hφ : ∀ (i : ι), DifferentiableOn 𝕜 (fun (x : E) => Φ x i) s) :
DifferentiableOn 𝕜 Φ s
source
theorem differentiableOn_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (s' : Set ((i : ι) → F' i)) :
DifferentiableOn 𝕜 (fun (f : (i : ι) → F' i) => f 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 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} (hφ : ∀ (i : ι), Differentiable 𝕜 fun (x : E) => Φ x i) :
Differentiable 𝕜 Φ
source
theorem differentiable_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_6} [Fintype ι] {F' : ι → Type u_7} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) :
Differentiable 𝕜 fun (f : (i : ι) → F' i) => f 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

### Derivatives of tuples `f : E → Π i : Fin n.succ, F' i` #

These can be used to prove results about functions of the form `fun x ↦ ![f x, g x, h x]`, as `Matrix.vecCons` is defeq to `Fin.cons`.

source
theorem hasStrictFDerivAt_finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] (i : Fin n.succ) → F' i} :
HasStrictFDerivAt (fun (x : E) => Fin.cons (φ x) (φs x)) φ' x ↔ HasStrictFDerivAt φ ((ContinuousLinearMap.proj 0).comp φ') x ∧ HasStrictFDerivAt φs ((Pi.compRightL 𝕜 F' Fin.succ).comp φ') x
source
theorem hasStrictFDerivAt_finCons' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ} :
HasStrictFDerivAt (fun (x : E) => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x ↔ HasStrictFDerivAt φ φ' x ∧ HasStrictFDerivAt φs φs' x

A variant of `hasStrictFDerivAt_finCons` where the derivative variables are free on the RHS instead.

source
theorem HasStrictFDerivAt.finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ} (h : HasStrictFDerivAt φ φ' x) (hs : HasStrictFDerivAt φs φs' x) :
HasStrictFDerivAt (fun (x : E) => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x
source
theorem hasFDerivAtFilter_finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] (i : Fin n.succ) → F' i} {l : Filter E} :
HasFDerivAtFilter (fun (x : E) => Fin.cons (φ x) (φs x)) φ' x l ↔ HasFDerivAtFilter φ ((ContinuousLinearMap.proj 0).comp φ') x l ∧ HasFDerivAtFilter φs ((Pi.compRightL 𝕜 F' Fin.succ).comp φ') x l
source
theorem hasFDerivAtFilter_finCons' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ} {l : Filter E} :
HasFDerivAtFilter (fun (x : E) => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x l ↔ HasFDerivAtFilter φ φ' x l ∧ HasFDerivAtFilter φs φs' x l

A variant of `hasFDerivAtFilter_finCons` where the derivative variables are free on the RHS instead.

source
theorem HasFDerivAtFilter.finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ} {l : Filter E} (h : HasFDerivAtFilter φ φ' x l) (hs : HasFDerivAtFilter φs φs' x l) :
HasFDerivAtFilter (fun (x : E) => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x l
source
theorem hasFDerivAt_finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] (i : Fin n.succ) → F' i} :
HasFDerivAt (fun (x : E) => Fin.cons (φ x) (φs x)) φ' x ↔ HasFDerivAt φ ((ContinuousLinearMap.proj 0).comp φ') x ∧ HasFDerivAt φs ((Pi.compRightL 𝕜 F' Fin.succ).comp φ') x
source
theorem hasFDerivAt_finCons' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ} :
HasFDerivAt (fun (x : E) => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x ↔ HasFDerivAt φ φ' x ∧ HasFDerivAt φs φs' x

A variant of `hasFDerivAt_finCons` where the derivative variables are free on the RHS instead.

source
theorem HasFDerivAt.finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ} (h : HasFDerivAt φ φ' x) (hs : HasFDerivAt φs φs' x) :
HasFDerivAt (fun (x : E) => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x
source
theorem hasFDerivWithinAt_finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] (i : Fin n.succ) → F' i} :
HasFDerivWithinAt (fun (x : E) => Fin.cons (φ x) (φs x)) φ' s x ↔ HasFDerivWithinAt φ ((ContinuousLinearMap.proj 0).comp φ') s x ∧ HasFDerivWithinAt φs ((Pi.compRightL 𝕜 F' Fin.succ).comp φ') s x
source
theorem hasFDerivWithinAt_finCons' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ} :
HasFDerivWithinAt (fun (x : E) => Fin.cons (φ x) (φs x)) (φ'.finCons φs') s x ↔ HasFDerivWithinAt φ φ' s x ∧ HasFDerivWithinAt φs φs' s x

A variant of `hasFDerivWithinAt_finCons` where the derivative variables are free on the RHS instead.

source
theorem HasFDerivWithinAt.finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ} (h : HasFDerivWithinAt φ φ' s x) (hs : HasFDerivWithinAt φs φs' s x) :
HasFDerivWithinAt (fun (x : E) => Fin.cons (φ x) (φs x)) (φ'.finCons φs') s x
source
theorem differentiableWithinAt_finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} :
DifferentiableWithinAt 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) s x ↔ DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x
source
theorem differentiableWithinAt_finCons' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} :
DifferentiableWithinAt 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) s x ↔ DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x

A variant of `differentiableWithinAt_finCons` where the derivative variables are free on the RHS instead.

source
theorem DifferentiableWithinAt.finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} (h : DifferentiableWithinAt 𝕜 φ s x) (hs : DifferentiableWithinAt 𝕜 φs s x) :
DifferentiableWithinAt 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) s x
source
theorem differentiableAt_finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} :
DifferentiableAt 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) x ↔ DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x
source
theorem differentiableAt_finCons' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} :
DifferentiableAt 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) x ↔ DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x

A variant of `differentiableAt_finCons` where the derivative variables are free on the RHS instead.

source
theorem DifferentiableAt.finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} (h : DifferentiableAt 𝕜 φ x) (hs : DifferentiableAt 𝕜 φs x) :
DifferentiableAt 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) x
source
theorem differentiableOn_finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} :
DifferentiableOn 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) s ↔ DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s
source
theorem differentiableOn_finCons' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} :
DifferentiableOn 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) s ↔ DifferentiableOn 𝕜 φ s ∧ DifferentiableOn 𝕜 φs s

A variant of `differentiableOn_finCons` where the derivative variables are free on the RHS instead.

source
theorem DifferentiableOn.finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} (h : DifferentiableOn 𝕜 φ s) (hs : DifferentiableOn 𝕜 φs s) :
DifferentiableOn 𝕜 (fun (x : E) => Fin.cons (φ x) (φs x)) s
source
theorem differentiable_finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} :
(Differentiable 𝕜 fun (x : E) => Fin.cons (φ x) (φs x)) ↔ Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs
source
theorem differentiable_finCons' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} :
(Differentiable 𝕜 fun (x : E) => Fin.cons (φ x) (φs x)) ↔ Differentiable 𝕜 φ ∧ Differentiable 𝕜 φs

A variant of `differentiable_finCons` where the derivative variables are free on the RHS instead.

source
theorem Differentiable.finCons {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {F' : Fin n.succ → Type u_6} [(i : Fin n.succ) → NormedAddCommGroup (F' i)] [(i : Fin n.succ) → NormedSpace 𝕜 (F' i)] {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} (h : Differentiable 𝕜 φ) (hs : Differentiable 𝕜 φs) :
Differentiable 𝕜 fun (x : E) => Fin.cons (φ x) (φs x)