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 #

source
theorem HasStrictFDerivAt.prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {f₁' : E β†’L[π•œ] F} {x : E} {fβ‚‚ : E β†’ G} {fβ‚‚' : E β†’L[π•œ] G} (hf₁ : HasStrictFDerivAt f₁ f₁' x) (hfβ‚‚ : HasStrictFDerivAt fβ‚‚ fβ‚‚' x) :
HasStrictFDerivAt (fun (x : E) => (f₁ x, fβ‚‚ x)) (f₁'.prod fβ‚‚') x
source
@[deprecated HasStrictFDerivAt.prodMk (since := "2025-03-09")]
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

Alias of HasStrictFDerivAt.prodMk.

source
theorem HasFDerivAtFilter.prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {f₁' : E β†’L[π•œ] F} {x : E} {L : Filter E} {fβ‚‚ : E β†’ G} {fβ‚‚' : E β†’L[π•œ] G} (hf₁ : HasFDerivAtFilter f₁ f₁' x L) (hfβ‚‚ : HasFDerivAtFilter fβ‚‚ fβ‚‚' x L) :
HasFDerivAtFilter (fun (x : E) => (f₁ x, fβ‚‚ x)) (f₁'.prod fβ‚‚') x L
source
@[deprecated HasFDerivAtFilter.prodMk (since := "2025-03-09")]
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

Alias of HasFDerivAtFilter.prodMk.

source
theorem HasFDerivWithinAt.prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {f₁' : E β†’L[π•œ] F} {x : E} {s : Set E} {fβ‚‚ : E β†’ G} {fβ‚‚' : E β†’L[π•œ] G} (hf₁ : HasFDerivWithinAt f₁ f₁' s x) (hfβ‚‚ : HasFDerivWithinAt fβ‚‚ fβ‚‚' s x) :
HasFDerivWithinAt (fun (x : E) => (f₁ x, fβ‚‚ x)) (f₁'.prod fβ‚‚') s x
source
@[deprecated HasFDerivWithinAt.prodMk (since := "2025-03-09")]
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

Alias of HasFDerivWithinAt.prodMk.

source
theorem HasFDerivAt.prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {f₁' : E β†’L[π•œ] F} {x : E} {fβ‚‚ : E β†’ G} {fβ‚‚' : E β†’L[π•œ] G} (hf₁ : HasFDerivAt f₁ f₁' x) (hfβ‚‚ : HasFDerivAt fβ‚‚ fβ‚‚' x) :
HasFDerivAt (fun (x : E) => (f₁ x, fβ‚‚ x)) (f₁'.prod fβ‚‚') x
source
@[deprecated HasFDerivAt.prodMk (since := "2025-03-09")]
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

Alias of HasFDerivAt.prodMk.

source
theorem hasFDerivAt_prodMk_left {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (eβ‚€ : E) (fβ‚€ : F) :
HasFDerivAt (fun (e : E) => (e, fβ‚€)) (ContinuousLinearMap.inl π•œ E F) eβ‚€
source
@[deprecated hasFDerivAt_prodMk_left (since := "2025-03-09")]
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β‚€

Alias of hasFDerivAt_prodMk_left.

source
theorem hasFDerivAt_prodMk_right {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] (eβ‚€ : E) (fβ‚€ : F) :
HasFDerivAt (fun (f : F) => (eβ‚€, f)) (ContinuousLinearMap.inr π•œ E F) fβ‚€
source
@[deprecated hasFDerivAt_prodMk_right (since := "2025-03-09")]
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β‚€

Alias of hasFDerivAt_prodMk_right.

source
theorem DifferentiableWithinAt.prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {x : E} {s : Set E} {fβ‚‚ : E β†’ G} (hf₁ : DifferentiableWithinAt π•œ f₁ s x) (hfβ‚‚ : DifferentiableWithinAt π•œ fβ‚‚ s x) :
DifferentiableWithinAt π•œ (fun (x : E) => (f₁ x, fβ‚‚ x)) s x
source
@[deprecated DifferentiableWithinAt.prodMk (since := "2025-03-09")]
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

Alias of DifferentiableWithinAt.prodMk.

source
@[simp]
theorem DifferentiableAt.prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {x : E} {fβ‚‚ : E β†’ G} (hf₁ : DifferentiableAt π•œ f₁ x) (hfβ‚‚ : DifferentiableAt π•œ fβ‚‚ x) :
DifferentiableAt π•œ (fun (x : E) => (f₁ x, fβ‚‚ x)) x
source
@[deprecated DifferentiableAt.prodMk (since := "2025-03-09")]
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

Alias of DifferentiableAt.prodMk.

source
theorem DifferentiableOn.prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {s : Set E} {fβ‚‚ : E β†’ G} (hf₁ : DifferentiableOn π•œ f₁ s) (hfβ‚‚ : DifferentiableOn π•œ fβ‚‚ s) :
DifferentiableOn π•œ (fun (x : E) => (f₁ x, fβ‚‚ x)) s
source
@[deprecated DifferentiableOn.prodMk (since := "2025-03-09")]
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

Alias of DifferentiableOn.prodMk.

source
@[simp]
theorem Differentiable.prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {fβ‚‚ : E β†’ G} (hf₁ : Differentiable π•œ f₁) (hfβ‚‚ : Differentiable π•œ fβ‚‚) :
Differentiable π•œ fun (x : E) => (f₁ x, fβ‚‚ x)
source
@[deprecated Differentiable.prodMk (since := "2025-03-09")]
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)

Alias of Differentiable.prodMk.

source
theorem DifferentiableAt.fderiv_prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {x : E} {fβ‚‚ : E β†’ G} (hf₁ : DifferentiableAt π•œ f₁ x) (hfβ‚‚ : DifferentiableAt π•œ fβ‚‚ x) :
fderiv π•œ (fun (x : E) => (f₁ x, fβ‚‚ x)) x = (fderiv π•œ f₁ x).prod (fderiv π•œ fβ‚‚ x)
source
@[deprecated DifferentiableAt.fderiv_prodMk (since := "2025-03-09")]
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)

Alias of DifferentiableAt.fderiv_prodMk.

source
theorem DifferentiableWithinAt.fderivWithin_prodMk {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {f₁ : E β†’ F} {x : E} {s : Set E} {fβ‚‚ : E β†’ G} (hf₁ : DifferentiableWithinAt π•œ f₁ s x) (hfβ‚‚ : DifferentiableWithinAt π•œ fβ‚‚ s x) (hxs : UniqueDiffWithinAt π•œ s x) :
fderivWithin π•œ (fun (x : E) => (f₁ x, fβ‚‚ x)) s x = (fderivWithin π•œ f₁ s x).prod (fderivWithin π•œ fβ‚‚ s x)
source
@[deprecated DifferentiableWithinAt.fderivWithin_prodMk (since := "2025-03-09")]
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)

Alias of DifferentiableWithinAt.fderivWithin_prodMk.

source
theorem hasStrictFDerivAt_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} :
HasStrictFDerivAt Prod.fst (ContinuousLinearMap.fst π•œ E F) p
source
theorem HasStrictFDerivAt.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} (h : HasStrictFDerivAt fβ‚‚ fβ‚‚' x) :
HasStrictFDerivAt (fun (x : E) => (fβ‚‚ x).1) ((ContinuousLinearMap.fst π•œ F G).comp fβ‚‚') x
source
theorem hasFDerivAtFilter_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} {L : Filter (E Γ— F)} :
HasFDerivAtFilter Prod.fst (ContinuousLinearMap.fst π•œ E F) p L
source
theorem HasFDerivAtFilter.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {L : Filter E} {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} (h : HasFDerivAtFilter fβ‚‚ fβ‚‚' x L) :
HasFDerivAtFilter (fun (x : E) => (fβ‚‚ x).1) ((ContinuousLinearMap.fst π•œ F G).comp fβ‚‚') x L
source
theorem hasFDerivAt_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} :
HasFDerivAt Prod.fst (ContinuousLinearMap.fst π•œ E F) p
source
theorem HasFDerivAt.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} (h : HasFDerivAt fβ‚‚ fβ‚‚' x) :
HasFDerivAt (fun (x : E) => (fβ‚‚ x).1) ((ContinuousLinearMap.fst π•œ F G).comp fβ‚‚') x
source
theorem hasFDerivWithinAt_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} {s : Set (E Γ— F)} :
HasFDerivWithinAt Prod.fst (ContinuousLinearMap.fst π•œ E F) s p
source
theorem HasFDerivWithinAt.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} (h : HasFDerivWithinAt fβ‚‚ fβ‚‚' s x) :
HasFDerivWithinAt (fun (x : E) => (fβ‚‚ x).1) ((ContinuousLinearMap.fst π•œ F G).comp fβ‚‚') s x
source
theorem differentiableAt_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} :
DifferentiableAt π•œ Prod.fst p
source
@[simp]
theorem DifferentiableAt.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {fβ‚‚ : E β†’ F Γ— G} (h : DifferentiableAt π•œ fβ‚‚ x) :
DifferentiableAt π•œ (fun (x : E) => (fβ‚‚ x).1) x
source
theorem differentiable_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] :
Differentiable π•œ Prod.fst
source
@[simp]
theorem Differentiable.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {fβ‚‚ : E β†’ F Γ— G} (h : Differentiable π•œ fβ‚‚) :
Differentiable π•œ fun (x : E) => (fβ‚‚ x).1
source
theorem differentiableWithinAt_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} {s : Set (E Γ— F)} :
DifferentiableWithinAt π•œ Prod.fst s p
source
theorem DifferentiableWithinAt.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {fβ‚‚ : E β†’ F Γ— G} (h : DifferentiableWithinAt π•œ fβ‚‚ s x) :
DifferentiableWithinAt π•œ (fun (x : E) => (fβ‚‚ x).1) s x
source
theorem differentiableOn_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set (E Γ— F)} :
DifferentiableOn π•œ Prod.fst s
source
theorem DifferentiableOn.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {s : Set E} {fβ‚‚ : E β†’ F Γ— G} (h : DifferentiableOn π•œ fβ‚‚ s) :
DifferentiableOn π•œ (fun (x : E) => (fβ‚‚ x).1) s
source
theorem fderiv_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} :
fderiv π•œ Prod.fst p = ContinuousLinearMap.fst π•œ E F
source
theorem fderiv.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {fβ‚‚ : E β†’ F Γ— G} (h : DifferentiableAt π•œ fβ‚‚ x) :
fderiv π•œ (fun (x : E) => (fβ‚‚ x).1) x = (ContinuousLinearMap.fst π•œ F G).comp (fderiv π•œ fβ‚‚ x)
source
theorem fderivWithin_fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} {s : Set (E Γ— F)} (hs : UniqueDiffWithinAt π•œ s p) :
fderivWithin π•œ Prod.fst s p = ContinuousLinearMap.fst π•œ E F
source
theorem fderivWithin.fst {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {fβ‚‚ : E β†’ F Γ— G} (hs : UniqueDiffWithinAt π•œ s x) (h : DifferentiableWithinAt π•œ fβ‚‚ s x) :
fderivWithin π•œ (fun (x : E) => (fβ‚‚ x).1) s x = (ContinuousLinearMap.fst π•œ F G).comp (fderivWithin π•œ fβ‚‚ s x)
source
theorem hasStrictFDerivAt_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} :
HasStrictFDerivAt Prod.snd (ContinuousLinearMap.snd π•œ E F) p
source
theorem HasStrictFDerivAt.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} (h : HasStrictFDerivAt fβ‚‚ fβ‚‚' x) :
HasStrictFDerivAt (fun (x : E) => (fβ‚‚ x).2) ((ContinuousLinearMap.snd π•œ F G).comp fβ‚‚') x
source
theorem hasFDerivAtFilter_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} {L : Filter (E Γ— F)} :
HasFDerivAtFilter Prod.snd (ContinuousLinearMap.snd π•œ E F) p L
source
theorem HasFDerivAtFilter.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {L : Filter E} {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} (h : HasFDerivAtFilter fβ‚‚ fβ‚‚' x L) :
HasFDerivAtFilter (fun (x : E) => (fβ‚‚ x).2) ((ContinuousLinearMap.snd π•œ F G).comp fβ‚‚') x L
source
theorem hasFDerivAt_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} :
HasFDerivAt Prod.snd (ContinuousLinearMap.snd π•œ E F) p
source
theorem HasFDerivAt.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} (h : HasFDerivAt fβ‚‚ fβ‚‚' x) :
HasFDerivAt (fun (x : E) => (fβ‚‚ x).2) ((ContinuousLinearMap.snd π•œ F G).comp fβ‚‚') x
source
theorem hasFDerivWithinAt_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} {s : Set (E Γ— F)} :
HasFDerivWithinAt Prod.snd (ContinuousLinearMap.snd π•œ E F) s p
source
theorem HasFDerivWithinAt.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {fβ‚‚ : E β†’ F Γ— G} {fβ‚‚' : E β†’L[π•œ] F Γ— G} (h : HasFDerivWithinAt fβ‚‚ fβ‚‚' s x) :
HasFDerivWithinAt (fun (x : E) => (fβ‚‚ x).2) ((ContinuousLinearMap.snd π•œ F G).comp fβ‚‚') s x
source
theorem differentiableAt_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} :
DifferentiableAt π•œ Prod.snd p
source
@[simp]
theorem DifferentiableAt.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {fβ‚‚ : E β†’ F Γ— G} (h : DifferentiableAt π•œ fβ‚‚ x) :
DifferentiableAt π•œ (fun (x : E) => (fβ‚‚ x).2) x
source
theorem differentiable_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] :
Differentiable π•œ Prod.snd
source
@[simp]
theorem Differentiable.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {fβ‚‚ : E β†’ F Γ— G} (h : Differentiable π•œ fβ‚‚) :
Differentiable π•œ fun (x : E) => (fβ‚‚ x).2
source
theorem differentiableWithinAt_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} {s : Set (E Γ— F)} :
DifferentiableWithinAt π•œ Prod.snd s p
source
theorem DifferentiableWithinAt.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {fβ‚‚ : E β†’ F Γ— G} (h : DifferentiableWithinAt π•œ fβ‚‚ s x) :
DifferentiableWithinAt π•œ (fun (x : E) => (fβ‚‚ x).2) s x
source
theorem differentiableOn_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set (E Γ— F)} :
DifferentiableOn π•œ Prod.snd s
source
theorem DifferentiableOn.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {s : Set E} {fβ‚‚ : E β†’ F Γ— G} (h : DifferentiableOn π•œ fβ‚‚ s) :
DifferentiableOn π•œ (fun (x : E) => (fβ‚‚ x).2) s
source
theorem fderiv_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} :
fderiv π•œ Prod.snd p = ContinuousLinearMap.snd π•œ E F
source
theorem fderiv.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {fβ‚‚ : E β†’ F Γ— G} (h : DifferentiableAt π•œ fβ‚‚ x) :
fderiv π•œ (fun (x : E) => (fβ‚‚ x).2) x = (ContinuousLinearMap.snd π•œ F G).comp (fderiv π•œ fβ‚‚ x)
source
theorem fderivWithin_snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {p : E Γ— F} {s : Set (E Γ— F)} (hs : UniqueDiffWithinAt π•œ s p) :
fderivWithin π•œ Prod.snd s p = ContinuousLinearMap.snd π•œ E F
source
theorem fderivWithin.snd {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {fβ‚‚ : E β†’ F Γ— G} (hs : UniqueDiffWithinAt π•œ s x) (h : DifferentiableWithinAt π•œ fβ‚‚ s x) :
fderivWithin π•œ (fun (x : E) => (fβ‚‚ x).2) s x = (ContinuousLinearMap.snd π•œ F G).comp (fderivWithin π•œ fβ‚‚ s x)
source
theorem HasStrictFDerivAt.prodMap {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace π•œ G'] {f : E β†’ F} {f' : E β†’L[π•œ] F} {fβ‚‚ : G β†’ G'} {fβ‚‚' : G β†’L[π•œ] G'} (p : E Γ— G) (hf : HasStrictFDerivAt f f' p.1) (hfβ‚‚ : HasStrictFDerivAt fβ‚‚ fβ‚‚' p.2) :
HasStrictFDerivAt (Prod.map f fβ‚‚) (f'.prodMap fβ‚‚') p
source
theorem HasFDerivAt.prodMap {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace π•œ G'] {f : E β†’ F} {f' : E β†’L[π•œ] F} {fβ‚‚ : G β†’ G'} {fβ‚‚' : G β†’L[π•œ] G'} (p : E Γ— G) (hf : HasFDerivAt f f' p.1) (hfβ‚‚ : HasFDerivAt fβ‚‚ fβ‚‚' p.2) :
HasFDerivAt (Prod.map f fβ‚‚) (f'.prodMap fβ‚‚') p
source
@[simp]
theorem DifferentiableAt.prodMap {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace π•œ G'] {f : E β†’ F} {fβ‚‚ : G β†’ G'} (p : E Γ— G) (hf : DifferentiableAt π•œ f p.1) (hfβ‚‚ : DifferentiableAt π•œ fβ‚‚ p.2) :
DifferentiableAt π•œ (fun (p : E Γ— G) => (f p.1, fβ‚‚ p.2)) p
source
@[deprecated DifferentiableAt.prodMap (since := "2025-03-09")]
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

Alias of DifferentiableAt.prodMap.

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:

source
@[simp]
theorem hasStrictFDerivAt_pi' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} {Ξ¦' : E β†’L[π•œ] (i : ΞΉ) β†’ F' i} :
HasStrictFDerivAt Ξ¦ Ξ¦' x ↔ βˆ€ (i : ΞΉ), HasStrictFDerivAt (fun (x : E) => Ξ¦ x i) ((ContinuousLinearMap.proj i).comp Ξ¦') x
source
theorem hasStrictFDerivAt_pi'' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} {Ξ¦' : E β†’L[π•œ] (i : ΞΉ) β†’ F' i} (hΟ† : βˆ€ (i : ΞΉ), HasStrictFDerivAt (fun (x : E) => Ξ¦ x i) ((ContinuousLinearMap.proj i).comp Ξ¦') x) :
HasStrictFDerivAt Ξ¦ Ξ¦' x
source
theorem hasStrictFDerivAt_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] (i : ΞΉ) (f : (i : ΞΉ) β†’ F' i) :
HasStrictFDerivAt (fun (f : (i : ΞΉ) β†’ F' i) => f i) (ContinuousLinearMap.proj i) f
source
@[simp]
theorem hasStrictFDerivAt_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ο† : (i : ΞΉ) β†’ E β†’ F' i} {Ο†' : (i : ΞΉ) β†’ E β†’L[π•œ] F' i} :
HasStrictFDerivAt (fun (x : E) (i : ΞΉ) => Ο† i x) (ContinuousLinearMap.pi Ο†') x ↔ βˆ€ (i : ΞΉ), HasStrictFDerivAt (Ο† i) (Ο†' i) x
source
@[simp]
theorem hasFDerivAtFilter_pi' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {L : Filter E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} {Ξ¦' : E β†’L[π•œ] (i : ΞΉ) β†’ F' i} :
HasFDerivAtFilter Ξ¦ Ξ¦' x L ↔ βˆ€ (i : ΞΉ), HasFDerivAtFilter (fun (x : E) => Ξ¦ x i) ((ContinuousLinearMap.proj i).comp Ξ¦') x L
source
theorem hasFDerivAtFilter_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {L : Filter E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ο† : (i : ΞΉ) β†’ E β†’ F' i} {Ο†' : (i : ΞΉ) β†’ E β†’L[π•œ] F' i} :
HasFDerivAtFilter (fun (x : E) (i : ΞΉ) => Ο† i x) (ContinuousLinearMap.pi Ο†') x L ↔ βˆ€ (i : ΞΉ), HasFDerivAtFilter (Ο† i) (Ο†' i) x L
source
@[simp]
theorem hasFDerivAt_pi' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} {Ξ¦' : E β†’L[π•œ] (i : ΞΉ) β†’ F' i} :
HasFDerivAt Ξ¦ Ξ¦' x ↔ βˆ€ (i : ΞΉ), HasFDerivAt (fun (x : E) => Ξ¦ x i) ((ContinuousLinearMap.proj i).comp Ξ¦') x
source
theorem hasFDerivAt_pi'' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} {Ξ¦' : E β†’L[π•œ] (i : ΞΉ) β†’ F' i} (hΟ† : βˆ€ (i : ΞΉ), HasFDerivAt (fun (x : E) => Ξ¦ x i) ((ContinuousLinearMap.proj i).comp Ξ¦') x) :
HasFDerivAt Ξ¦ Ξ¦' x
source
theorem hasFDerivAt_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] (i : ΞΉ) (f : (i : ΞΉ) β†’ F' i) :
HasFDerivAt (fun (f : (i : ΞΉ) β†’ F' i) => f i) (ContinuousLinearMap.proj i) f
source
theorem hasFDerivAt_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ο† : (i : ΞΉ) β†’ E β†’ F' i} {Ο†' : (i : ΞΉ) β†’ E β†’L[π•œ] F' i} :
HasFDerivAt (fun (x : E) (i : ΞΉ) => Ο† i x) (ContinuousLinearMap.pi Ο†') x ↔ βˆ€ (i : ΞΉ), HasFDerivAt (Ο† i) (Ο†' i) x
source
@[simp]
theorem hasFDerivWithinAt_pi' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} {Ξ¦' : E β†’L[π•œ] (i : ΞΉ) β†’ F' i} :
HasFDerivWithinAt Ξ¦ Ξ¦' s x ↔ βˆ€ (i : ΞΉ), HasFDerivWithinAt (fun (x : E) => Ξ¦ x i) ((ContinuousLinearMap.proj i).comp Ξ¦') s x
source
theorem hasFDerivWithinAt_pi'' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} {Ξ¦' : E β†’L[π•œ] (i : ΞΉ) β†’ F' i} (hΟ† : βˆ€ (i : ΞΉ), HasFDerivWithinAt (fun (x : E) => Ξ¦ x i) ((ContinuousLinearMap.proj i).comp Ξ¦') s x) :
HasFDerivWithinAt Ξ¦ Ξ¦' s x
source
theorem hasFDerivWithinAt_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] (i : ΞΉ) (f : (i : ΞΉ) β†’ F' i) (s' : Set ((i : ΞΉ) β†’ F' i)) :
HasFDerivWithinAt (fun (f : (i : ΞΉ) β†’ F' i) => f i) (ContinuousLinearMap.proj i) s' f
source
theorem hasFDerivWithinAt_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ο† : (i : ΞΉ) β†’ E β†’ F' i} {Ο†' : (i : ΞΉ) β†’ E β†’L[π•œ] F' i} :
HasFDerivWithinAt (fun (x : E) (i : ΞΉ) => Ο† i x) (ContinuousLinearMap.pi Ο†') s x ↔ βˆ€ (i : ΞΉ), HasFDerivWithinAt (Ο† i) (Ο†' i) s x
source
@[simp]
theorem differentiableWithinAt_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} :
DifferentiableWithinAt π•œ Ξ¦ s x ↔ βˆ€ (i : ΞΉ), DifferentiableWithinAt π•œ (fun (x : E) => Ξ¦ x i) s x
source
theorem differentiableWithinAt_pi'' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} (hΟ† : βˆ€ (i : ΞΉ), DifferentiableWithinAt π•œ (fun (x : E) => Ξ¦ x i) s x) :
DifferentiableWithinAt π•œ Ξ¦ s x
source
theorem differentiableWithinAt_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] (i : ΞΉ) (f : (i : ΞΉ) β†’ F' i) (s' : Set ((i : ΞΉ) β†’ F' i)) :
DifferentiableWithinAt π•œ (fun (f : (i : ΞΉ) β†’ F' i) => f i) s' f
source
@[simp]
theorem differentiableAt_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} :
DifferentiableAt π•œ Ξ¦ x ↔ βˆ€ (i : ΞΉ), DifferentiableAt π•œ (fun (x : E) => Ξ¦ x i) x
source
theorem differentiableAt_pi'' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} (hΟ† : βˆ€ (i : ΞΉ), DifferentiableAt π•œ (fun (x : E) => Ξ¦ x i) x) :
DifferentiableAt π•œ Ξ¦ x
source
theorem differentiableAt_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] (i : ΞΉ) (f : (i : ΞΉ) β†’ F' i) :
DifferentiableAt π•œ (fun (f : (i : ΞΉ) β†’ F' i) => f i) f
source
theorem differentiableOn_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} :
DifferentiableOn π•œ Ξ¦ s ↔ βˆ€ (i : ΞΉ), DifferentiableOn π•œ (fun (x : E) => Ξ¦ x i) s
source
theorem differentiableOn_pi'' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} (hΟ† : βˆ€ (i : ΞΉ), DifferentiableOn π•œ (fun (x : E) => Ξ¦ x i) s) :
DifferentiableOn π•œ Ξ¦ s
source
theorem differentiableOn_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] (i : ΞΉ) (s' : Set ((i : ΞΉ) β†’ F' i)) :
DifferentiableOn π•œ (fun (f : (i : ΞΉ) β†’ F' i) => f i) s'
source
theorem differentiable_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} :
Differentiable π•œ Ξ¦ ↔ βˆ€ (i : ΞΉ), Differentiable π•œ fun (x : E) => Ξ¦ x i
source
theorem differentiable_pi'' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ξ¦ : E β†’ (i : ΞΉ) β†’ F' i} (hΟ† : βˆ€ (i : ΞΉ), Differentiable π•œ fun (x : E) => Ξ¦ x i) :
Differentiable π•œ Ξ¦
source
theorem differentiable_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] (i : ΞΉ) :
Differentiable π•œ fun (f : (i : ΞΉ) β†’ F' i) => f i
source
theorem fderivWithin_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ο† : (i : ΞΉ) β†’ E β†’ F' i} (h : βˆ€ (i : ΞΉ), DifferentiableWithinAt π•œ (Ο† i) s x) (hs : UniqueDiffWithinAt π•œ s x) :
fderivWithin π•œ (fun (x : E) (i : ΞΉ) => Ο† i x) s x = ContinuousLinearMap.pi fun (i : ΞΉ) => fderivWithin π•œ (Ο† i) s x
source
theorem fderiv_pi {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {F' : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (F' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (F' i)] {Ο† : (i : ΞΉ) β†’ E β†’ F' i} (h : βˆ€ (i : ΞΉ), DifferentiableAt π•œ (Ο† i) x) :
fderiv π•œ (fun (x : E) (i : ΞΉ) => Ο† i x) x = ContinuousLinearMap.pi fun (i : ΞΉ) => fderiv π•œ (Ο† i) x

Derivatives of tuples f : E β†’ Ξ  i : Fin n.succ, F' i #

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

source
theorem hasStrictFDerivAt_finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] (i : Fin n.succ) β†’ F' i} :
HasStrictFDerivAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) Ο†' x ↔ HasStrictFDerivAt Ο† ((ContinuousLinearMap.proj 0).comp Ο†') x ∧ HasStrictFDerivAt Ο†s ((Pi.compRightL π•œ F' Fin.succ).comp Ο†') x
source
theorem hasStrictFDerivAt_finCons' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] F' 0} {Ο†s' : E β†’L[π•œ] (i : Fin n) β†’ F' i.succ} :
HasStrictFDerivAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) (Ο†'.finCons Ο†s') x ↔ HasStrictFDerivAt Ο† Ο†' x ∧ HasStrictFDerivAt Ο†s Ο†s' x

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

source
theorem HasStrictFDerivAt.finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] F' 0} {Ο†s' : E β†’L[π•œ] (i : Fin n) β†’ F' i.succ} (h : HasStrictFDerivAt Ο† Ο†' x) (hs : HasStrictFDerivAt Ο†s Ο†s' x) :
HasStrictFDerivAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) (Ο†'.finCons Ο†s') x
source
theorem hasFDerivAtFilter_finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] (i : Fin n.succ) β†’ F' i} {l : Filter E} :
HasFDerivAtFilter (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) Ο†' x l ↔ HasFDerivAtFilter Ο† ((ContinuousLinearMap.proj 0).comp Ο†') x l ∧ HasFDerivAtFilter Ο†s ((Pi.compRightL π•œ F' Fin.succ).comp Ο†') x l
source
theorem hasFDerivAtFilter_finCons' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] F' 0} {Ο†s' : E β†’L[π•œ] (i : Fin n) β†’ F' i.succ} {l : Filter E} :
HasFDerivAtFilter (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) (Ο†'.finCons Ο†s') x l ↔ HasFDerivAtFilter Ο† Ο†' x l ∧ HasFDerivAtFilter Ο†s Ο†s' x l

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

source
theorem HasFDerivAtFilter.finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] F' 0} {Ο†s' : E β†’L[π•œ] (i : Fin n) β†’ F' i.succ} {l : Filter E} (h : HasFDerivAtFilter Ο† Ο†' x l) (hs : HasFDerivAtFilter Ο†s Ο†s' x l) :
HasFDerivAtFilter (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) (Ο†'.finCons Ο†s') x l
source
theorem hasFDerivAt_finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] (i : Fin n.succ) β†’ F' i} :
HasFDerivAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) Ο†' x ↔ HasFDerivAt Ο† ((ContinuousLinearMap.proj 0).comp Ο†') x ∧ HasFDerivAt Ο†s ((Pi.compRightL π•œ F' Fin.succ).comp Ο†') x
source
theorem hasFDerivAt_finCons' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] F' 0} {Ο†s' : E β†’L[π•œ] (i : Fin n) β†’ F' i.succ} :
HasFDerivAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) (Ο†'.finCons Ο†s') x ↔ HasFDerivAt Ο† Ο†' x ∧ HasFDerivAt Ο†s Ο†s' x

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

source
theorem HasFDerivAt.finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] F' 0} {Ο†s' : E β†’L[π•œ] (i : Fin n) β†’ F' i.succ} (h : HasFDerivAt Ο† Ο†' x) (hs : HasFDerivAt Ο†s Ο†s' x) :
HasFDerivAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) (Ο†'.finCons Ο†s') x
source
theorem hasFDerivWithinAt_finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] (i : Fin n.succ) β†’ F' i} :
HasFDerivWithinAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) Ο†' s x ↔ HasFDerivWithinAt Ο† ((ContinuousLinearMap.proj 0).comp Ο†') s x ∧ HasFDerivWithinAt Ο†s ((Pi.compRightL π•œ F' Fin.succ).comp Ο†') s x
source
theorem hasFDerivWithinAt_finCons' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] F' 0} {Ο†s' : E β†’L[π•œ] (i : Fin n) β†’ F' i.succ} :
HasFDerivWithinAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) (Ο†'.finCons Ο†s') s x ↔ HasFDerivWithinAt Ο† Ο†' s x ∧ HasFDerivWithinAt Ο†s Ο†s' s x

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

source
theorem HasFDerivWithinAt.finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} {Ο†' : E β†’L[π•œ] F' 0} {Ο†s' : E β†’L[π•œ] (i : Fin n) β†’ F' i.succ} (h : HasFDerivWithinAt Ο† Ο†' s x) (hs : HasFDerivWithinAt Ο†s Ο†s' s x) :
HasFDerivWithinAt (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) (Ο†'.finCons Ο†s') s x
source
theorem differentiableWithinAt_finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} :
DifferentiableWithinAt π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) s x ↔ DifferentiableWithinAt π•œ Ο† s x ∧ DifferentiableWithinAt π•œ Ο†s s x
source
theorem differentiableWithinAt_finCons' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} :
DifferentiableWithinAt π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) s x ↔ DifferentiableWithinAt π•œ Ο† s x ∧ DifferentiableWithinAt π•œ Ο†s s x

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

source
theorem DifferentiableWithinAt.finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} (h : DifferentiableWithinAt π•œ Ο† s x) (hs : DifferentiableWithinAt π•œ Ο†s s x) :
DifferentiableWithinAt π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) s x
source
theorem differentiableAt_finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} :
DifferentiableAt π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) x ↔ DifferentiableAt π•œ Ο† x ∧ DifferentiableAt π•œ Ο†s x
source
theorem differentiableAt_finCons' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} :
DifferentiableAt π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) x ↔ DifferentiableAt π•œ Ο† x ∧ DifferentiableAt π•œ Ο†s x

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

source
theorem DifferentiableAt.finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} (h : DifferentiableAt π•œ Ο† x) (hs : DifferentiableAt π•œ Ο†s x) :
DifferentiableAt π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) x
source
theorem differentiableOn_finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} :
DifferentiableOn π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) s ↔ DifferentiableOn π•œ Ο† s ∧ DifferentiableOn π•œ Ο†s s
source
theorem differentiableOn_finCons' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} :
DifferentiableOn π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) s ↔ DifferentiableOn π•œ Ο† s ∧ DifferentiableOn π•œ Ο†s s

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

source
theorem DifferentiableOn.finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} (h : DifferentiableOn π•œ Ο† s) (hs : DifferentiableOn π•œ Ο†s s) :
DifferentiableOn π•œ (fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) s
source
theorem differentiable_finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} :
(Differentiable π•œ fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) ↔ Differentiable π•œ Ο† ∧ Differentiable π•œ Ο†s
source
theorem differentiable_finCons' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} :
(Differentiable π•œ fun (x : E) => Fin.cons (Ο† x) (Ο†s x)) ↔ Differentiable π•œ Ο† ∧ Differentiable π•œ Ο†s

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

source
theorem Differentiable.finCons {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {n : β„•} {F' : Fin n.succ β†’ Type u_6} [(i : Fin n.succ) β†’ NormedAddCommGroup (F' i)] [(i : Fin n.succ) β†’ NormedSpace π•œ (F' i)] {Ο† : E β†’ F' 0} {Ο†s : E β†’ (i : Fin n) β†’ F' i.succ} (h : Differentiable π•œ Ο†) (hs : Differentiable π•œ Ο†s) :
Differentiable π•œ fun (x : E) => Fin.cons (Ο† x) (Ο†s x)