Genuine parameter regularity of the forced initial value problem

The homogeneous evolutions need not have assumed parameter derivatives. The constructed solution is the actual inverse of a smooth Volterra operator on a fixed continuous-path Banach space. Operator inversion therefore proves its parameter smoothness from coefficient and data smoothness alone.

theorem EulerLinearDuhamel.Evolution.volterraInverse_eq_mapInverse {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (U : Evolution T hT B) : U.volterraInverse = (volterraOperator T hT B).inverse

The constructed Volterra inverse is the canonical continuous-linear-map inverse.

theorem EulerLinearDuhamel.Evolution.solution_eq_volterraInverse {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (U : Evolution T hT B) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : U.solution f a₀ = U.volterraInverse ((ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T)) a₀ + (EulerContinuousTimeIntegral.integral T hT) f)

The actual forced solution is obtained by this genuine Volterra inverse.

theorem EulerLinearDuhamel.volterraOperator_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (B : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) {n : WithTop ℕ∞} (hB : ContDiff ℝ n B) : ContDiff ℝ n fun (x : P) => volterraOperator T hT (B x)

Smooth coefficients give a genuinely smooth Volterra operator family.

theorem EulerLinearDuhamel.volterraInverse_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (B : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (U : (x : P) → Evolution T hT (B x)) {n : WithTop ℕ∞} (hB : ContDiff ℝ n B) : ContDiff ℝ n fun (x : P) => (U x).volterraInverse

Parameter smoothness of the actual inverse requires no parameter regularity assumption on the chosen homogeneous fundamental evolutions.

theorem EulerLinearDuhamel.solution_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (B : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (U : (x : P) → Evolution T hT (B x)) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → E) {n : WithTop ℕ∞} (hB : ContDiff ℝ n B) (hf : ContDiff ℝ n f) (ha₀ : ContDiff ℝ n a₀) : ContDiff ℝ n fun (x : P) => (U x).solution (f x) (a₀ x)

The integral construction is genuinely smooth in parameters whenever the coefficient, initial data and forcing are smooth in their actual Banach norms.