A continuous Banach-valued path has its strong time derivative once that derivative is continuous and is verified through a separating family of bounded linear observations. The proof reconstructs the actual Bochner primitive and does not infer strong convergence from pointwise convergence.
theorem
EulerSeparatingTimeDerivative.eq_initial_add_integral
{E : Type u_1}
{F : Type u_2}
{I : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(f g : C(↑(Set.Icc 0 T), E))
(L : I → E →L[ℝ] F)
(hsep : Function.Injective fun (u : E) (i : I) => (L i) u)
(hd :
∀ (i : I) (t : ℝ) (ht : t ∈ Set.Ioo 0 T),
HasDerivAt (fun (r : ℝ) => (L i) (EulerVolterraConvolution.extendPath T hT f r)) ((L i) (g ⟨t, ⋯⟩)) t)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerSeparatingTimeDerivative.hasDerivWithinAt
{E : Type u_1}
{F : Type u_2}
{I : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(f g : C(↑(Set.Icc 0 T), E))
(L : I → E →L[ℝ] F)
(hsep : Function.Injective fun (u : E) (i : I) => (L i) u)
(hd :
∀ (i : I) (t : ℝ) (ht : t ∈ Set.Ioo 0 T),
HasDerivAt (fun (r : ℝ) => (L i) (EulerVolterraConvolution.extendPath T hT f r)) ((L i) (g ⟨t, ⋯⟩)) t)
(t : ↑(Set.Icc 0 T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT f) (g t) (Set.Icc 0 T) ↑t
theorem
EulerSeparatingTimeDerivative.hasDerivAt
{E : Type u_1}
{F : Type u_2}
{I : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(f g : C(↑(Set.Icc 0 T), E))
(L : I → E →L[ℝ] F)
(hsep : Function.Injective fun (u : E) (i : I) => (L i) u)
(hd :
∀ (i : I) (t : ℝ) (ht : t ∈ Set.Ioo 0 T),
HasDerivAt (fun (r : ℝ) => (L i) (EulerVolterraConvolution.extendPath T hT f r)) ((L i) (g ⟨t, ⋯⟩)) t)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (EulerVolterraConvolution.extendPath T hT f) (g ⟨t, ⋯⟩) t