Lifting an actual continuous evolution equation through an injective bounded linear map.
theorem
EulerInjectivePathDerivative.map_pathIntegral
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
(L : E →L[ℝ] F)
(T : ℝ)
(hT : 0 ≤ T)
(a b : ℝ)
(f : C(↑(Set.Icc 0 T), E))
:
L ((EulerIntegralPathLimit.pathIntegralOperator T hT a b) f) = (EulerIntegralPathLimit.pathIntegralOperator T hT a b)
((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) L) f)
A bounded linear map commutes with the integral of an actual continuous time path.
theorem
EulerInjectivePathDerivative.integral_equation_of_injective_map
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
(L : E →L[ℝ] F)
(hL : Function.Injective ⇑L)
(T : ℝ)
(hT : 0 ≤ T)
(u f : C(↑(Set.Icc 0 T), E))
(hd :
∀ t ∈ Set.Ioo 0 T,
HasDerivAt (fun (r : ℝ) => L (EulerVolterraConvolution.extendPath T hT u r))
(L (EulerVolterraConvolution.extendPath T hT f t)) t)
(t : ↑(Set.Icc 0 T))
:
An evolution equation in the weaker space gives its exact integral equation in the stronger space when the embedding is injective and the proposed derivative is continuous there.
theorem
EulerInjectivePathDerivative.hasDerivAt_of_injective_map
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
(L : E →L[ℝ] F)
(hL : Function.Injective ⇑L)
(T : ℝ)
(hT : 0 ≤ T)
(u f : C(↑(Set.Icc 0 T), E))
(hd :
∀ t ∈ Set.Ioo 0 T,
HasDerivAt (fun (r : ℝ) => L (EulerVolterraConvolution.extendPath T hT u r))
(L (EulerVolterraConvolution.extendPath T hT f t)) t)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (EulerVolterraConvolution.extendPath T hT u) (EulerVolterraConvolution.extendPath T hT f t) t
A continuous stronger-space right-hand side lifts a genuine derivative equation through an injective bounded embedding, without assuming the stronger derivative exists.