Documentation

Mathlib.Analysis.Calculus.Deriv.Prod

Derivatives of functions taking values in product types #

In this file we prove lemmas about derivatives of functions f : 𝕜 → E × F and of functions f : 𝕜 → (Π i, E i).

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

Keywords #

derivative

Derivative of the cartesian product of two functions #

theorem HasDerivAtFilter.prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {L : Filter 𝕜} {G : Type w} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₂ : 𝕜 → G} {f₂' : G} (hf₁ : HasDerivAtFilter f₁ f₁' x L) (hf₂ : HasDerivAtFilter f₂ f₂' x L) :
HasDerivAtFilter (fun x => (f₁ x, f₂ x)) (f₁', f₂') x L
theorem HasDerivWithinAt.prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {s : Set 𝕜} {G : Type w} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₂ : 𝕜 → G} {f₂' : G} (hf₁ : HasDerivWithinAt f₁ f₁' s x) (hf₂ : HasDerivWithinAt f₂ f₂' s x) :
HasDerivWithinAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') s x
theorem HasDerivAt.prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {G : Type w} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₂ : 𝕜 → G} {f₂' : G} (hf₁ : HasDerivAt f₁ f₁' x) (hf₂ : HasDerivAt f₂ f₂' x) :
HasDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x
theorem HasStrictDerivAt.prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ : 𝕜 → F} {f₁' : F} {x : 𝕜} {G : Type w} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f₂ : 𝕜 → G} {f₂' : G} (hf₁ : HasStrictDerivAt f₁ f₁' x) (hf₂ : HasStrictDerivAt f₂ f₂' x) :
HasStrictDerivAt (fun x => (f₁ x, f₂ x)) (f₁', f₂') x

Derivatives of functions f : 𝕜 → Π i, E i #

@[simp]
theorem hasStrictDerivAt_pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_1} [Fintype ι] {E' : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i} {φ' : (i : ι) → E' i} :
HasStrictDerivAt φ φ' x ↔ ∀ (i : ι), HasStrictDerivAt (fun x => φ x i) (φ' i) x
@[simp]
theorem hasDerivAtFilter_pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {L : Filter 𝕜} {ι : Type u_1} [Fintype ι] {E' : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i} {φ' : (i : ι) → E' i} :
HasDerivAtFilter φ φ' x L ↔ ∀ (i : ι), HasDerivAtFilter (fun x => φ x i) (φ' i) x L
theorem hasDerivAt_pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_1} [Fintype ι] {E' : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i} {φ' : (i : ι) → E' i} :
HasDerivAt φ φ' x ↔ ∀ (i : ι), HasDerivAt (fun x => φ x i) (φ' i) x
theorem hasDerivWithinAt_pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} [Fintype ι] {E' : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i} {φ' : (i : ι) → E' i} :
HasDerivWithinAt φ φ' s x ↔ ∀ (i : ι), HasDerivWithinAt (fun x => φ x i) (φ' i) s x
theorem derivWithin_pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_1} [Fintype ι] {E' : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i} (h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => φ x i) s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin φ s x = fun i => derivWithin (fun x => φ x i) s x
theorem deriv_pi {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_1} [Fintype ι] {E' : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i} (h : ∀ (i : ι), DifferentiableAt 𝕜 (fun x => φ x i) x) :
deriv φ x = fun i => deriv (fun x => φ x i) x