Naturality of the actual Duhamel solution #
A bounded linear map intertwining the coefficient operators also intertwines the actual forced solutions. This follows from their differential equations and uniqueness; no compatibility of the chosen homogeneous fundamental maps is assumed. In particular it applies to inclusions and support-changing spatial translations.
theorem
EulerLinearDuhamel.Evolution.solution_map
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
{T : ℝ}
{hT : 0 ≤ T}
{B : C(↑(Set.Icc 0 T), E →L[ℝ] E)}
{D : C(↑(Set.Icc 0 T), F →L[ℝ] F)}
(U : Evolution T hT B)
(V : Evolution T hT D)
(L : E →L[ℝ] F)
(hL : ∀ (t : ↑(Set.Icc 0 T)) (u : E), (D t) (L u) = L ((B t) u))
(f : C(↑(Set.Icc 0 T), E))
(a₀ : E)
:
V.solution ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) L) f) (L a₀) = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) L) (U.solution f a₀)
Bounded linear intertwiners commute with the actual forced solution.
theorem
EulerLinearDuhamel.Evolution.solution_map_apply
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
{T : ℝ}
{hT : 0 ≤ T}
{B : C(↑(Set.Icc 0 T), E →L[ℝ] E)}
{D : C(↑(Set.Icc 0 T), F →L[ℝ] F)}
(U : Evolution T hT B)
(V : Evolution T hT D)
(L : E →L[ℝ] F)
(hL : ∀ (t : ↑(Set.Icc 0 T)) (u : E), (D t) (L u) = L ((B t) u))
(f : C(↑(Set.Icc 0 T), E))
(a₀ : E)
(t : ↑(Set.Icc 0 T))
:
Pointwise form of the same identity, including both endpoints.