# 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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {fβ : E β F} {fβ' : E βL[π] F} {x : E} {L : } {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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] (eβ : E) (fβ : F) :
HasFDerivAt (fun (f : F) => (eβ, f)) (ContinuousLinearMap.inr π E F) fβ
theorem DifferentiableWithinAt.prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
HasStrictFDerivAt Prod.fst (ContinuousLinearMap.fst π E F) p
theorem HasStrictFDerivAt.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} {L : Filter (E Γ F)} :
HasFDerivAtFilter Prod.fst (ContinuousLinearMap.fst π E F) p L
theorem HasFDerivAtFilter.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {L : } {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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
HasFDerivAt Prod.fst (ContinuousLinearMap.fst π E F) p
theorem HasFDerivAt.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} {s : Set (E Γ F)} :
HasFDerivWithinAt Prod.fst (ContinuousLinearMap.fst π E F) s p
theorem HasFDerivWithinAt.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
DifferentiableAt π Prod.fst p
@[simp]
theorem DifferentiableAt.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] :
Differentiable π Prod.fst
@[simp]
theorem Differentiable.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {fβ : E β F Γ G} (h : Differentiable π fβ) :
Differentiable π fun (x : E) => (fβ x).1
theorem differentiableWithinAt_fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} {s : Set (E Γ F)} :
DifferentiableWithinAt π Prod.fst s p
theorem DifferentiableWithinAt.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {s : Set (E Γ F)} :
DifferentiableOn π Prod.fst s
theorem DifferentiableOn.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
fderiv π Prod.fst p = ContinuousLinearMap.fst π E F
theorem fderiv.fst {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
HasStrictFDerivAt Prod.snd (ContinuousLinearMap.snd π E F) p
theorem HasStrictFDerivAt.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} {L : Filter (E Γ F)} :
HasFDerivAtFilter Prod.snd (ContinuousLinearMap.snd π E F) p L
theorem HasFDerivAtFilter.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {L : } {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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
HasFDerivAt Prod.snd (ContinuousLinearMap.snd π E F) p
theorem HasFDerivAt.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} {s : Set (E Γ F)} :
HasFDerivWithinAt Prod.snd (ContinuousLinearMap.snd π E F) s p
theorem HasFDerivWithinAt.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
DifferentiableAt π Prod.snd p
@[simp]
theorem DifferentiableAt.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] :
Differentiable π Prod.snd
@[simp]
theorem Differentiable.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {fβ : E β F Γ G} (h : Differentiable π fβ) :
Differentiable π fun (x : E) => (fβ x).2
theorem differentiableWithinAt_snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} {s : Set (E Γ F)} :
DifferentiableWithinAt π Prod.snd s p
theorem DifferentiableWithinAt.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {s : Set (E Γ F)} :
DifferentiableOn π Prod.snd s
theorem DifferentiableOn.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {p : E Γ F} :
fderiv π Prod.snd p = ContinuousLinearMap.snd π E F
theorem fderiv.snd {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [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} [] {E : Type u_2} [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) (.comp Ξ¦') x
theorem hasStrictFDerivAt_pi'' {π : Type u_1} [] {E : Type u_2} [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) (.comp Ξ¦') x) :
HasStrictFDerivAt Ξ¦ Ξ¦' x
theorem hasStrictFDerivAt_apply {π : Type u_1} [] {ΞΉ : 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) f
@[simp]
theorem hasStrictFDerivAt_pi {π : Type u_1} [] {E : Type u_2} [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) () x β β (i : ΞΉ), HasStrictFDerivAt (Ο i) (Ο' i) x
@[simp]
theorem hasFDerivAtFilter_pi' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {L : } {ΞΉ : 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) (.comp Ξ¦') x L
theorem hasFDerivAtFilter_pi {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {L : } {ΞΉ : 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) () x L β β (i : ΞΉ), HasFDerivAtFilter (Ο i) (Ο' i) x L
@[simp]
theorem hasFDerivAt_pi' {π : Type u_1} [] {E : Type u_2} [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) (.comp Ξ¦') x
theorem hasFDerivAt_pi'' {π : Type u_1} [] {E : Type u_2} [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) (.comp Ξ¦') x) :
HasFDerivAt Ξ¦ Ξ¦' x
theorem hasFDerivAt_apply {π : Type u_1} [] {ΞΉ : 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) f
theorem hasFDerivAt_pi {π : Type u_1} [] {E : Type u_2} [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) () x β β (i : ΞΉ), HasFDerivAt (Ο i) (Ο' i) x
@[simp]
theorem hasFDerivWithinAt_pi' {π : Type u_1} [] {E : Type u_2} [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) (.comp Ξ¦') s x
theorem hasFDerivWithinAt_pi'' {π : Type u_1} [] {E : Type u_2} [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) (.comp Ξ¦') s x) :
HasFDerivWithinAt Ξ¦ Ξ¦' s x
theorem hasFDerivWithinAt_apply {π : Type u_1} [] {ΞΉ : 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) s' f
theorem hasFDerivWithinAt_pi {π : Type u_1} [] {E : Type u_2} [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) () s x β β (i : ΞΉ), HasFDerivWithinAt (Ο i) (Ο' i) s x
@[simp]
theorem differentiableWithinAt_pi {π : Type u_1} [] {E : Type u_2} [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} [] {E : Type u_2} [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} [] {ΞΉ : 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} [] {E : Type u_2} [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} [] {E : Type u_2} [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} [] {ΞΉ : 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} [] {E : Type u_2} [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} [] {E : Type u_2} [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} [] {ΞΉ : 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} [] {E : Type u_2} [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} [] {E : Type u_2} [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} [] {ΞΉ : 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} [] {E : Type u_2} [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} [] {E : Type u_2} [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