Documentation

Mathlib.Analysis.Calculus.FDeriv.Prod

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:

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