# mathlib3documentation

analysis.calculus.deriv.prod

# Derivatives of functions taking values in product types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 has_deriv_at_filter.prod {𝕜 : Type u} {F : Type v} [ F] {f₁ : 𝕜 F} {f₁' : F} {x : 𝕜} {L : filter 𝕜} {G : Type w} [ G] {f₂ : 𝕜 G} {f₂' : G} (hf₁ : f₁' x L) (hf₂ : f₂' x L) :
has_deriv_at_filter (λ (x : 𝕜), (f₁ x, f₂ x)) (f₁', f₂') x L
theorem has_deriv_within_at.prod {𝕜 : Type u} {F : Type v} [ F] {f₁ : 𝕜 F} {f₁' : F} {x : 𝕜} {s : set 𝕜} {G : Type w} [ G] {f₂ : 𝕜 G} {f₂' : G} (hf₁ : f₁' s x) (hf₂ : f₂' s x) :
has_deriv_within_at (λ (x : 𝕜), (f₁ x, f₂ x)) (f₁', f₂') s x
theorem has_deriv_at.prod {𝕜 : Type u} {F : Type v} [ F] {f₁ : 𝕜 F} {f₁' : F} {x : 𝕜} {G : Type w} [ G] {f₂ : 𝕜 G} {f₂' : G} (hf₁ : f₁' x) (hf₂ : f₂' x) :
has_deriv_at (λ (x : 𝕜), (f₁ x, f₂ x)) (f₁', f₂') x
theorem has_strict_deriv_at.prod {𝕜 : Type u} {F : Type v} [ F] {f₁ : 𝕜 F} {f₁' : F} {x : 𝕜} {G : Type w} [ G] {f₂ : 𝕜 G} {f₂' : G} (hf₁ : f₁' x) (hf₂ : f₂' x) :
has_strict_deriv_at (λ (x : 𝕜), (f₁ x, f₂ x)) (f₁', f₂') x

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

@[simp]
theorem has_strict_deriv_at_pi {𝕜 : Type u} {x : 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), (E' i)] {φ : 𝕜 Π (i : ι), E' i} {φ' : Π (i : ι), E' i} :
x (i : ι), has_strict_deriv_at (λ (x : 𝕜), φ x i) (φ' i) x
@[simp]
theorem has_deriv_at_filter_pi {𝕜 : Type u} {x : 𝕜} {L : filter 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), (E' i)] {φ : 𝕜 Π (i : ι), E' i} {φ' : Π (i : ι), E' i} :
x L (i : ι), has_deriv_at_filter (λ (x : 𝕜), φ x i) (φ' i) x L
theorem has_deriv_at_pi {𝕜 : Type u} {x : 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), (E' i)] {φ : 𝕜 Π (i : ι), E' i} {φ' : Π (i : ι), E' i} :
φ' x (i : ι), has_deriv_at (λ (x : 𝕜), φ x i) (φ' i) x
theorem has_deriv_within_at_pi {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), (E' i)] {φ : 𝕜 Π (i : ι), E' i} {φ' : Π (i : ι), E' i} :
s x (i : ι), has_deriv_within_at (λ (x : 𝕜), φ x i) (φ' i) s x
theorem deriv_within_pi {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), (E' i)] {φ : 𝕜 Π (i : ι), E' i} (h : (i : ι), (λ (x : 𝕜), φ x i) s x) (hs : x) :
s x = λ (i : ι), deriv_within (λ (x : 𝕜), φ x i) s x
theorem deriv_pi {𝕜 : Type u} {x : 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), (E' i)] {φ : 𝕜 Π (i : ι), E' i} (h : (i : ι), (λ (x : 𝕜), φ x i) x) :
x = λ (i : ι), deriv (λ (x : 𝕜), φ x i) x