Derivatives of operations on continuous alternating maps #
In this file we prove formulas for the derivatives of
ContinuousAlternatingMap.compContinuousLinearMap, the pullback of a continuous alternating map along a continuous linear map;- application of a
ContinuousAlternatingMapas a function of both the map and the vectors.
Derivative of the pullback #
In this section we prove a formula for the derivative of the pullback of a continuous alternating map along a continuous linear map, as a function of both maps.
theorem
ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{G : Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → G [⋀^ι]→L[𝕜] H}
{f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
{x : E}
[Finite ι]
:
HasStrictFDerivAt (toContinuousMultilinearMap ∘ f) ((toContinuousMultilinearMapCLM 𝕜).comp f') x ↔ HasStrictFDerivAt f f' x
theorem
ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap
{𝕜 : Type u_1}
{ι : Type u_2}
{F : Type u_4}
{G : Type u_5}
{H : Type u_6}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
[Fintype ι]
[DecidableEq ι]
(fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G))
:
HasStrictFDerivAt (fun (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)) => fg.1.compContinuousLinearMap fg.2)
((compContinuousLinearMapCLM fg.2).comp (ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G)) + (fg.1.fderivCompContinuousLinearMap fg.2).comp (ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G)))
fg
theorem
HasStrictFDerivAt.continuousAlternatingMapCompContinuousLinearMap
{𝕜 : 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]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → G [⋀^ι]→L[𝕜] H}
{f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
{g : E → F →L[𝕜] G}
{g' : E →L[𝕜] F →L[𝕜] G}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : HasStrictFDerivAt f f' x)
(hg : HasStrictFDerivAt g g' x)
:
HasStrictFDerivAt (fun (x : E) => (f x).compContinuousLinearMap (g x))
((ContinuousAlternatingMap.compContinuousLinearMapCLM (g x)).comp f' + ((f x).fderivCompContinuousLinearMap (g x)).comp g')
x
theorem
HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap
{𝕜 : 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]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → G [⋀^ι]→L[𝕜] H}
{f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
{g : E → F →L[𝕜] G}
{g' : E →L[𝕜] F →L[𝕜] G}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : HasFDerivAt f f' x)
(hg : HasFDerivAt g g' x)
:
HasFDerivAt (fun (x : E) => (f x).compContinuousLinearMap (g x))
((ContinuousAlternatingMap.compContinuousLinearMapCLM (g x)).comp f' + ((f x).fderivCompContinuousLinearMap (g x)).comp g')
x
theorem
HasFDerivWithinAt.continuousAlternatingMapCompContinuousLinearMap
{𝕜 : 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]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → G [⋀^ι]→L[𝕜] H}
{f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
{g : E → F →L[𝕜] G}
{g' : E →L[𝕜] F →L[𝕜] G}
{s : Set E}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : HasFDerivWithinAt f f' s x)
(hg : HasFDerivWithinAt g g' s x)
:
HasFDerivWithinAt (fun (x : E) => (f x).compContinuousLinearMap (g x))
((ContinuousAlternatingMap.compContinuousLinearMapCLM (g x)).comp f' + ((f x).fderivCompContinuousLinearMap (g x)).comp g')
s x
theorem
fderivWithin_continuousAlternatingMapCompContinuousLinearMap
{𝕜 : 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]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → G [⋀^ι]→L[𝕜] H}
{g : E → F →L[𝕜] G}
{s : Set E}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : DifferentiableWithinAt 𝕜 f s x)
(hg : DifferentiableWithinAt 𝕜 g s x)
(hs : UniqueDiffWithinAt 𝕜 s x)
:
fderivWithin 𝕜 (fun (x : E) => (f x).compContinuousLinearMap (g x)) s x = (ContinuousAlternatingMap.compContinuousLinearMapCLM (g x)).comp (fderivWithin 𝕜 f s x) + ((f x).fderivCompContinuousLinearMap (g x)).comp (fderivWithin 𝕜 g s x)
theorem
fderiv_continuousAlternatingMapCompContinuousLinearMap
{𝕜 : 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]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → G [⋀^ι]→L[𝕜] H}
{g : E → F →L[𝕜] G}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : DifferentiableAt 𝕜 f x)
(hg : DifferentiableAt 𝕜 g x)
:
fderiv 𝕜 (fun (x : E) => (f x).compContinuousLinearMap (g x)) x = (ContinuousAlternatingMap.compContinuousLinearMapCLM (g x)).comp (fderiv 𝕜 f x) + ((f x).fderivCompContinuousLinearMap (g x)).comp (fderiv 𝕜 g x)
Differentiability of the pullback #
In this section we prove that the pullback of a continuous alternating map along a continuous linear map is differentiable with respect to a parameter, provided that both maps are differentiable.
theorem
DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMap
{𝕜 : 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]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → G [⋀^ι]→L[𝕜] H}
{g : E → F →L[𝕜] G}
{s : Set E}
{x : E}
[Finite ι]
(hf : DifferentiableWithinAt 𝕜 f s x)
(hg : DifferentiableWithinAt 𝕜 g s x)
:
DifferentiableWithinAt 𝕜 (fun (x : E) => (f x).compContinuousLinearMap (g x)) s x
theorem
DifferentiableAt.continuousAlternatingMapCompContinuousLinearMap
{𝕜 : 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]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
[NormedAddCommGroup H]
[NormedSpace 𝕜 H]
{f : E → G [⋀^ι]→L[𝕜] H}
{g : E → F →L[𝕜] G}
{x : E}
[Finite ι]
(hf : DifferentiableAt 𝕜 f x)
(hg : DifferentiableAt 𝕜 g x)
:
DifferentiableAt 𝕜 (fun (x : E) => (f x).compContinuousLinearMap (g x)) x
Derivative of a continuous alternating map applied to a tuple of vectors #
In this section we prove the formula for the derivative D_xf(x; g_0(x), ..., g_n(x)).
theorem
ContinuousAlternatingMap.hasStrictFDerivAt
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[Fintype ι]
[DecidableEq ι]
(f : E [⋀^ι]→L[𝕜] F)
(x : ι → E)
:
HasStrictFDerivAt (⇑f) (f.linearDeriv x) x
theorem
ContinuousAlternatingMap.hasFDerivAt
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[Fintype ι]
[DecidableEq ι]
(f : E [⋀^ι]→L[𝕜] F)
(x : ι → E)
:
HasFDerivAt (⇑f) (f.linearDeriv x) x
theorem
ContinuousAlternatingMap.hasFDerivWithinAt
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[Fintype ι]
[DecidableEq ι]
(f : E [⋀^ι]→L[𝕜] F)
(s : Set (ι → E))
(x : ι → E)
:
HasFDerivWithinAt (⇑f) (f.linearDeriv x) s x
theorem
HasStrictFDerivAt.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
{g' : ι → E →L[𝕜] F}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : HasStrictFDerivAt f f' x)
(hg : ∀ (i : ι), HasStrictFDerivAt (g i) (g' i) x)
:
HasStrictFDerivAt (fun (x : E) => (f x) fun (x_1 : ι) => g x_1 x)
((ContinuousAlternatingMap.apply 𝕜 F G fun (x_1 : ι) => g x_1 x).comp f' + ∑ i : ι, ((f x).toContinuousLinearMap (fun (x_1 : ι) => g x_1 x) i).comp (g' i))
x
theorem
HasFDerivAt.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
{g' : ι → E →L[𝕜] F}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : HasFDerivAt f f' x)
(hg : ∀ (i : ι), HasFDerivAt (g i) (g' i) x)
:
HasFDerivAt (fun (x : E) => (f x) fun (x_1 : ι) => g x_1 x)
((ContinuousAlternatingMap.apply 𝕜 F G fun (x_1 : ι) => g x_1 x).comp f' + ∑ i : ι, ((f x).toContinuousLinearMap (fun (x_1 : ι) => g x_1 x) i).comp (g' i))
x
theorem
HasFDerivWithinAt.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{f' : E →L[𝕜] F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
{g' : ι → E →L[𝕜] F}
{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) fun (x_1 : ι) => g x_1 x)
((ContinuousAlternatingMap.apply 𝕜 F G fun (x_1 : ι) => g x_1 x).comp f' + ∑ i : ι, ((f x).toContinuousLinearMap (fun (x_1 : ι) => g x_1 x) i).comp (g' i))
s x
theorem
fderivWithin_continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
{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) fun (x_1 : ι) => g x_1 x) s x = (ContinuousAlternatingMap.apply 𝕜 F G fun (x_1 : ι) => g x_1 x).comp (fderivWithin 𝕜 f s x) + ∑ i : ι, ((f x).toContinuousLinearMap (fun (x_1 : ι) => g x_1 x) i).comp (fderivWithin 𝕜 (g i) s x)
theorem
fderiv_continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
{x : E}
[Fintype ι]
[DecidableEq ι]
(hf : DifferentiableAt 𝕜 f x)
(hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x)
:
fderiv 𝕜 (fun (x : E) => (f x) fun (x_1 : ι) => g x_1 x) x = (ContinuousAlternatingMap.apply 𝕜 F G fun (x_1 : ι) => g x_1 x).comp (fderiv 𝕜 f x) + ∑ i : ι, ((f x).toContinuousLinearMap (fun (x_1 : ι) => g x_1 x) i).comp (fderiv 𝕜 (g i) x)
theorem
DifferentiableWithinAt.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
{s : Set E}
{x : E}
[Finite ι]
(hf : DifferentiableWithinAt 𝕜 f s x)
(hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x)
:
DifferentiableWithinAt 𝕜 (fun (x : E) => (f x) fun (x_1 : ι) => g x_1 x) s x
theorem
DifferentiableAt.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
{x : E}
[Finite ι]
(hf : DifferentiableAt 𝕜 f x)
(hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x)
:
DifferentiableAt 𝕜 (fun (x : E) => (f x) fun (x_1 : ι) => g x_1 x) x
theorem
DifferentiableOn.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
{s : Set E}
[Finite ι]
(hf : DifferentiableOn 𝕜 f s)
(hg : ∀ (i : ι), DifferentiableOn 𝕜 (g i) s)
:
DifferentiableOn 𝕜 (fun (x : E) => (f x) fun (x_1 : ι) => g x_1 x) s
theorem
Differentiable.continuousAlternatingMap_apply
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
{G : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F [⋀^ι]→L[𝕜] G}
{g : ι → E → F}
[Finite ι]
(hf : Differentiable 𝕜 f)
(hg : ∀ (i : ι), Differentiable 𝕜 (g i))
:
Differentiable 𝕜 fun (x : E) => (f x) fun (x_1 : ι) => g x_1 x
theorem
ContinuousAlternatingMap.differentiable
{𝕜 : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[Finite ι]
(f : E [⋀^ι]→L[𝕜] F)
:
Differentiable 𝕜 ⇑f