mathlib3 documentation

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} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f₁ : 𝕜 F} {f₁' : F} {x : 𝕜} {L : filter 𝕜} {G : Type w} [normed_add_comm_group G] [normed_space 𝕜 G] {f₂ : 𝕜 G} {f₂' : G} (hf₁ : has_deriv_at_filter f₁ f₁' x L) (hf₂ : has_deriv_at_filter f₂ f₂' x L) :
has_deriv_at_filter (λ (x : 𝕜), (f₁ x, f₂ x)) (f₁', f₂') x L
theorem has_deriv_within_at.prod {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f₁ : 𝕜 F} {f₁' : F} {x : 𝕜} {s : set 𝕜} {G : Type w} [normed_add_comm_group G] [normed_space 𝕜 G] {f₂ : 𝕜 G} {f₂' : G} (hf₁ : has_deriv_within_at f₁ f₁' s x) (hf₂ : has_deriv_within_at f₂ f₂' s x) :
has_deriv_within_at (λ (x : 𝕜), (f₁ x, f₂ x)) (f₁', f₂') s x
theorem has_deriv_at.prod {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f₁ : 𝕜 F} {f₁' : F} {x : 𝕜} {G : Type w} [normed_add_comm_group G] [normed_space 𝕜 G] {f₂ : 𝕜 G} {f₂' : G} (hf₁ : has_deriv_at f₁ f₁' x) (hf₂ : has_deriv_at f₂ f₂' x) :
has_deriv_at (λ (x : 𝕜), (f₁ x, f₂ x)) (f₁', f₂') x
theorem has_strict_deriv_at.prod {𝕜 : Type u} [nontrivially_normed_field 𝕜] {F : Type v} [normed_add_comm_group F] [normed_space 𝕜 F] {f₁ : 𝕜 F} {f₁' : F} {x : 𝕜} {G : Type w} [normed_add_comm_group G] [normed_space 𝕜 G] {f₂ : 𝕜 G} {f₂' : G} (hf₁ : has_strict_deriv_at f₁ f₁' x) (hf₂ : has_strict_deriv_at f₂ 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} [nontrivially_normed_field 𝕜] {x : 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), normed_space 𝕜 (E' i)] {φ : 𝕜 Π (i : ι), E' i} {φ' : Π (i : ι), E' i} :
has_strict_deriv_at φ φ' x (i : ι), has_strict_deriv_at (λ (x : 𝕜), φ x i) (φ' i) x
@[simp]
theorem has_deriv_at_filter_pi {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {L : filter 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), normed_space 𝕜 (E' i)] {φ : 𝕜 Π (i : ι), E' i} {φ' : Π (i : ι), E' i} :
has_deriv_at_filter φ φ' x L (i : ι), has_deriv_at_filter (λ (x : 𝕜), φ x i) (φ' i) x L
theorem has_deriv_at_pi {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), normed_space 𝕜 (E' i)] {φ : 𝕜 Π (i : ι), E' i} {φ' : Π (i : ι), E' i} :
has_deriv_at φ φ' x (i : ι), has_deriv_at (λ (x : 𝕜), φ x i) (φ' i) x
theorem has_deriv_within_at_pi {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), normed_space 𝕜 (E' i)] {φ : 𝕜 Π (i : ι), E' i} {φ' : Π (i : ι), E' i} :
has_deriv_within_at φ φ' s x (i : ι), has_deriv_within_at (λ (x : 𝕜), φ x i) (φ' i) s x
theorem deriv_within_pi {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {s : set 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), normed_space 𝕜 (E' i)] {φ : 𝕜 Π (i : ι), E' i} (h : (i : ι), differentiable_within_at 𝕜 (λ (x : 𝕜), φ x i) s x) (hs : unique_diff_within_at 𝕜 s x) :
deriv_within φ s x = λ (i : ι), deriv_within (λ (x : 𝕜), φ x i) s x
theorem deriv_pi {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {ι : Type u_1} [fintype ι] {E' : ι Type u_2} [Π (i : ι), normed_add_comm_group (E' i)] [Π (i : ι), normed_space 𝕜 (E' i)] {φ : 𝕜 Π (i : ι), E' i} (h : (i : ι), differentiable_at 𝕜 (λ (x : 𝕜), φ x i) x) :
deriv φ x = λ (i : ι), deriv (λ (x : 𝕜), φ x i) x