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