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) :