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

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)) (f₁'.prod f₂') x

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)) (f₁'.prod f₂') x L

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)) (f₁'.prod f₂') s x

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)) (f₁'.prod f₂') x

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₀

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₀

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

@[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

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

@[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)

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 = (fderiv 𝕜 f₁ x).prod (fderiv 𝕜 f₂ x)

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 = (fderivWithin 𝕜 f₁ s x).prod (fderivWithin 𝕜 f₂ s x)

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

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

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

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

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

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

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

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

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

@[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

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

@[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

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

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

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

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

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

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)

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

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)

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

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

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

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

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

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

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

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

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

@[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

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

@[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

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

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

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

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

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

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)

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

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)

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

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

@[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 Φ.

@[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

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

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

@[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

@[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

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

@[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

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

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

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

@[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

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

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

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

@[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

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

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

@[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

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

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

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

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

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'

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

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 𝕜 Φ

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

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

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.

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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)