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
Mathlib/Analysis/Calculus/Deriv/Basic.lean.
Keywords #
derivative
Derivative of the Cartesian product of two functions #
theorem
HasDerivAtFilter.prodMk
{𝕜 : 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)
:
@[deprecated HasDerivAtFilter.prodMk (since := "2025-03-09")]
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)
:
Alias of HasDerivAtFilter.prodMk.
theorem
HasDerivWithinAt.prodMk
{𝕜 : 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)
:
@[deprecated HasDerivWithinAt.prodMk (since := "2025-03-09")]
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)
:
Alias of HasDerivWithinAt.prodMk.
theorem
HasDerivAt.prodMk
{𝕜 : 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)
:
@[deprecated HasDerivAt.prodMk (since := "2025-03-09")]
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)
:
Alias of HasDerivAt.prodMk.
theorem
HasStrictDerivAt.prodMk
{𝕜 : 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)
:
@[deprecated HasStrictDerivAt.prodMk (since := "2025-03-09")]
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)
:
Alias of HasStrictDerivAt.prodMk.
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}
:
@[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}
:
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}
:
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}
:
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)
:
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)
:
Derivatives of tuples f : 𝕜 → Π i : Fin n.succ, F' i #
These can be used to prove results about functions of the form fun x ↦ ![f x, g x, h x],
as Matrix.vecCons is defeq to Fin.cons.
theorem
hasStrictDerivAt_finCons
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : (i : Fin n.succ) → F' i}
:
HasStrictDerivAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) φ' x ↔ HasStrictDerivAt φ (φ' 0) x ∧ HasStrictDerivAt φs (fun (i : Fin n) => φ' i.succ) x
theorem
hasStrictDerivAt_finCons'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : F' 0}
{φs' : (i : Fin n) → F' i.succ}
:
HasStrictDerivAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x ↔ HasStrictDerivAt φ φ' x ∧ HasStrictDerivAt φs φs' x
A variant of hasStrictDerivAt_finCons where the derivative variables are free on the RHS
instead.
theorem
HasStrictDerivAt.finCons
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : F' 0}
{φs' : (i : Fin n) → F' i.succ}
(h : HasStrictDerivAt φ φ' x)
(hs : HasStrictDerivAt φs φs' x)
:
HasStrictDerivAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x
theorem
hasDerivAtFilter_finCons
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : (i : Fin n.succ) → F' i}
{l : Filter 𝕜}
:
HasDerivAtFilter (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) φ' x l ↔ HasDerivAtFilter φ (φ' 0) x l ∧ HasDerivAtFilter φs (fun (i : Fin n) => φ' i.succ) x l
theorem
hasDerivAtFilter_finCons'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : F' 0}
{φs' : (i : Fin n) → F' i.succ}
{l : Filter 𝕜}
:
HasDerivAtFilter (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x l ↔ HasDerivAtFilter φ φ' x l ∧ HasDerivAtFilter φs φs' x l
A variant of hasDerivAtFilter_finCons where the derivative variables are free on the RHS
instead.
theorem
HasDerivAtFilter.finCons
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : F' 0}
{φs' : (i : Fin n) → F' i.succ}
{l : Filter 𝕜}
(h : HasDerivAtFilter φ φ' x l)
(hs : HasDerivAtFilter φs φs' x l)
:
HasDerivAtFilter (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x l
theorem
hasDerivAt_finCons
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : (i : Fin n.succ) → F' i}
:
HasDerivAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) φ' x ↔ HasDerivAt φ (φ' 0) x ∧ HasDerivAt φs (fun (i : Fin n) => φ' i.succ) x
theorem
hasDerivAt_finCons'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : F' 0}
{φs' : (i : Fin n) → F' i.succ}
:
HasDerivAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x ↔ HasDerivAt φ φ' x ∧ HasDerivAt φs φs' x
A variant of hasDerivAt_finCons where the derivative variables are free on the RHS
instead.
theorem
HasDerivAt.finCons
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : F' 0}
{φs' : (i : Fin n) → F' i.succ}
(h : HasDerivAt φ φ' x)
(hs : HasDerivAt φs φs' x)
:
HasDerivAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') x
theorem
hasDerivWithinAt_finCons
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : (i : Fin n.succ) → F' i}
:
HasDerivWithinAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) φ' s x ↔ HasDerivWithinAt φ (φ' 0) s x ∧ HasDerivWithinAt φs (fun (i : Fin n) => φ' i.succ) s x
theorem
hasDerivWithinAt_finCons'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : F' 0}
{φs' : (i : Fin n) → F' i.succ}
:
HasDerivWithinAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x ↔ HasDerivWithinAt φ φ' s x ∧ HasDerivWithinAt φs φs' s x
A variant of hasDerivWithinAt_finCons where the derivative variables are free on the RHS
instead.
theorem
HasDerivWithinAt.finCons
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{n : ℕ}
{F' : Fin n.succ → Type u_1}
[(i : Fin n.succ) → NormedAddCommGroup (F' i)]
[(i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
{φ : 𝕜 → F' 0}
{φs : 𝕜 → (i : Fin n) → F' i.succ}
{φ' : F' 0}
{φs' : (i : Fin n) → F' i.succ}
(h : HasDerivWithinAt φ φ' s x)
(hs : HasDerivWithinAt φs φs' s x)
:
HasDerivWithinAt (fun (x : 𝕜) => Fin.cons (φ x) (φs x)) (Fin.cons φ' φs') s x