Derivatives of operations on continuous multilinear maps #
In this file,
ιis an index type (Fin nin many applications);E,F i,G i,H, are normed spaces for eachi : ι;f xis a continuous multilinear map fromΠ i, G itoH, depending on a parameterx : E;- for each
i : ι,g i xis a continuous linear mapF i → G i, depending on a parameterx : E.
Given this data, for each x we can define a continuous multilinear map from Π i, F i to H
given by (f x).compContinuousLinearMap (fun i ↦ g i x) v = f x (fun i ↦ g i x (v i)).
As a map between functional spaces,
ContinuousMultilinearMap.compContinuousLinearMap is multilinear in (f; g i).
Thus its derivative with respect to each map (f or g i)
is given by substituting f' or g' i instead of f or g i
in (f x).compContinuousLinearMap (fun i ↦ g i x),
and the full differential is given by the sum of these terms.
In terms of bundled maps, the derivative with respect to f
is given by ContinuousMultilinearMap.compContinuousLinearMapL
and the sum of terms that represent the derivatives with respect to g i
is given by ContinuousMultilinearMap.fderivCompContinuousLinearMap.
All statements in the first section are claiming this, for various notions of differentiation.
The second section deduces the corresponding differentiability results when ι is finite.
theorem
ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
[Fintype ι]
[DecidableEq ι]
(fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i))
:
HasStrictFDerivAt
(fun (fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → F i →L[𝕜] G i)) => fg.1.compContinuousLinearMap fg.2)
((compContinuousLinearMapL fg.2).comp
(ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)) + (fg.1.fderivCompContinuousLinearMap fg.2).comp
(ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H) ((i : ι) → F i →L[𝕜] G i)))
fg
theorem
HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
{g' : (i : ι) → E →L[𝕜] F i →L[𝕜] G i}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : HasStrictFDerivAt f f' x)
(hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x)
:
HasStrictFDerivAt (fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x)
((ContinuousMultilinearMap.compContinuousLinearMapL fun (x_1 : ι) => g x_1 x).comp f' + ((f x).fderivCompContinuousLinearMap fun (x_1 : ι) => g x_1 x).comp (ContinuousLinearMap.pi g'))
x
theorem
HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
{g' : (i : ι) → E →L[𝕜] F i →L[𝕜] G i}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : HasFDerivAt f f' x)
(hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x)
:
HasFDerivAt (fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x)
((ContinuousMultilinearMap.compContinuousLinearMapL fun (x_1 : ι) => g x_1 x).comp f' + ((f x).fderivCompContinuousLinearMap fun (x_1 : ι) => g x_1 x).comp (ContinuousLinearMap.pi g'))
x
theorem
HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{f' : E →L[𝕜] ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
{g' : (i : ι) → E →L[𝕜] F i →L[𝕜] G i}
{s : Set E}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : HasFDerivWithinAt f f' s x)
(hg : ∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x)
:
HasFDerivWithinAt (fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x)
((ContinuousMultilinearMap.compContinuousLinearMapL fun (x_1 : ι) => g x_1 x).comp f' + ((f x).fderivCompContinuousLinearMap fun (x_1 : ι) => g x_1 x).comp (ContinuousLinearMap.pi g'))
s x
theorem
fderivWithin_continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
{s : Set E}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : DifferentiableWithinAt 𝕜 f s x)
(hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x)
(hs : UniqueDiffWithinAt 𝕜 s x)
:
fderivWithin 𝕜 (fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x) s x = (ContinuousMultilinearMap.compContinuousLinearMapL fun (x_1 : ι) => g x_1 x).comp (fderivWithin 𝕜 f s x) + ((f x).fderivCompContinuousLinearMap fun (x_1 : ι) => g x_1 x).comp
(ContinuousLinearMap.pi fun (i : ι) => fderivWithin 𝕜 (g i) s x)
theorem
fderiv_continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : DifferentiableAt 𝕜 f x)
(hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x)
:
fderiv 𝕜 (fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x) x = (ContinuousMultilinearMap.compContinuousLinearMapL fun (x_1 : ι) => g x_1 x).comp (fderiv 𝕜 f x) + ((f x).fderivCompContinuousLinearMap fun (x_1 : ι) => g x_1 x).comp
(ContinuousLinearMap.pi fun (i : ι) => fderiv 𝕜 (g i) x)
theorem
DifferentiableWithinAt.continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
{s : Set E}
{x : E}
[Finite ι]
(hf : DifferentiableWithinAt 𝕜 f s x)
(hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x)
:
DifferentiableWithinAt 𝕜 (fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x) s x
theorem
DifferentiableAt.continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
{x : E}
[Finite ι]
(hf : DifferentiableAt 𝕜 f x)
(hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x)
:
DifferentiableAt 𝕜 (fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x) x
theorem
DifferentiableOn.continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
{s : Set E}
[Finite ι]
(hf : DifferentiableOn 𝕜 f s)
(hg : ∀ (i : ι), DifferentiableOn 𝕜 (g i) s)
:
DifferentiableOn 𝕜 (fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x) s
theorem
Differentiable.continuousMultilinearMapCompContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : ι → Type u_4}
{G : ι → Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[(i : ι) → NormedAddCommGroup (F i)]
[(i : ι) → NormedSpace 𝕜 (F i)]
[(i : ι) → NormedAddCommGroup (G i)]
[(i : ι) → NormedSpace 𝕜 (G i)]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → ContinuousMultilinearMap 𝕜 G H}
{g : (i : ι) → E → F i →L[𝕜] G i}
[Finite ι]
(hf : Differentiable 𝕜 f)
(hg : ∀ (i : ι), Differentiable 𝕜 (g i))
:
Differentiable 𝕜 fun (x : E) => (f x).compContinuousLinearMap fun (x_1 : ι) => g x_1 x