The actual bounded solution and Volterra inverse

The Duhamel integral is a bounded linear map in the forcing and initial data. It gives a two-sided inverse for the continuous-path Volterra operator. This unweighted inverse is used only for qualitative parameter regularity; source quantitative estimates use the original relative propagator bound directly.

noncomputable def EulerLinearDuhamel.Evolution.forcingOperator {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) : C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), E)

The actual zero-initial-data forcing operator.

Equations

• U.forcingOperator = EulerContinuousTimeIntegral.multiplier U.forward ∘SL EulerContinuousTimeIntegral.integral T hT ∘SL EulerContinuousTimeIntegral.multiplier U.backward

noncomputable def EulerLinearDuhamel.Evolution.initialOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (U : Evolution T hT B) : E →L[ℝ] C(↑(Set.Icc 0 T), E)

The actual homogeneous initial-data operator.

Equations

• U.initialOperator = EulerContinuousTimeIntegral.multiplier U.forward ∘SL ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T) ∘SL U.backward ⟨0, ⋯⟩

theorem EulerLinearDuhamel.Evolution.forcingOperator_eq {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)) : U.forcingOperator f = U.solution f 0

The bounded forcing operator is exactly the Duhamel construction.

theorem EulerLinearDuhamel.Evolution.solution_eq_operators {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.initialOperator a₀ + U.forcingOperator f

Splitting the actual forced solution into its two bounded data maps.

theorem EulerLinearDuhamel.Evolution.forcingOperator_profile_bound {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)) (g : ↑(Set.Icc 0 T) → ℝ) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hg₀ : g ⟨0, ⋯⟩ = 1) (C D : ℝ) (hC : 0 ≤ C) (hU : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ‖U.propagator t s‖ ≤ C * g t / g s) (hf : ∀ (s : ↑(Set.Icc 0 T)), ‖f s‖ ≤ D * g s) (t : ↑(Set.Icc 0 T)) : ‖(U.forcingOperator f) t‖ ≤ C * g t * ↑t * D

The original relative propagator bound controls the actual forcing map.

theorem EulerLinearDuhamel.Evolution.initialOperator_profile_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (U : Evolution T hT B) (a₀ : E) (g : ↑(Set.Icc 0 T) → ℝ) (hg₀ : g ⟨0, ⋯⟩ = 1) (C : ℝ) (hU : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ‖U.propagator t s‖ ≤ C * g t / g s) (t : ↑(Set.Icc 0 T)) : ‖(U.initialOperator a₀) t‖ ≤ C * g t * ‖a₀‖

The homogeneous initial-data map has the same profile and propagator constant.

theorem EulerLinearDuhamel.Evolution.solution_integral {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₀ = (ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T)) a₀ + (EulerContinuousTimeIntegral.integral T hT) ((EulerContinuousTimeIntegral.multiplier B) (U.solution f a₀) + f)

The forced path satisfies the actual integral equation.

noncomputable def EulerLinearDuhamel.volterraOperator {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), E)

The ordinary continuous-path Volterra operator.

Equations

• EulerLinearDuhamel.volterraOperator T hT B = ContinuousLinearMap.id ℝ C(↑(Set.Icc 0 T), E) - EulerContinuousTimeIntegral.integral T hT ∘SL EulerContinuousTimeIntegral.multiplier B

noncomputable def EulerLinearDuhamel.Evolution.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) : C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), E)

Duhamel's formula gives an actual inverse on every continuous input.

Equations

• U.volterraInverse = ContinuousLinearMap.id ℝ C(↑(Set.Icc 0 T), E) + U.forcingOperator ∘SL EulerContinuousTimeIntegral.multiplier B

theorem EulerLinearDuhamel.Evolution.volterra_operator_inverse {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) (h : C(↑(Set.Icc 0 T), E)) : (volterraOperator T hT B) (U.volterraInverse h) = h

The Volterra operator followed by the constructed inverse is the identity.

theorem EulerLinearDuhamel.Evolution.volterraOperator_injective {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) : Function.Injective ⇑(volterraOperator T hT B)

The homogeneous Volterra equation has only its zero solution.

theorem EulerLinearDuhamel.Evolution.volterra_inverse_operator {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) (h : C(↑(Set.Icc 0 T), E)) : U.volterraInverse ((volterraOperator T hT B) h) = h

The constructed inverse is also a left inverse.

noncomputable def EulerLinearDuhamel.Evolution.volterraEquiv {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) : C(↑(Set.Icc 0 T), E) ≃L[ℝ] C(↑(Set.Icc 0 T), E)

The actual two-sided Volterra equivalence.

Equations

• U.volterraEquiv = ContinuousLinearEquiv.equivOfInverse (EulerLinearDuhamel.volterraOperator T hT B) U.volterraInverse ⋯ ⋯