Duhamel operators in the source's time profile

The bounded Green operator in the normalized continuous-path space inherits its constant directly from the relative homogeneous propagator bound. The frozen-coefficient identity is exact and will be differentiated for quantitative parameter estimates; no norm of the weighted primitive is used.

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

The actual homogeneous data map, normalized by the profile.

Equations

• U.weightedInitial g hg = EulerContinuousTimeWeight.normalize g hg ∘SL U.initialOperator

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

The actual Green map for forcing measured in the source profile.

Equations

• U.weightedForcing g hg = EulerContinuousTimeWeight.normalize g hg ∘SL U.forcingOperator ∘SL EulerContinuousTimeWeight.weight g

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

The initial-data norm uses just the relative propagator constant.

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

The Green-operator norm is interval length times the relative propagator constant. Neither the maximum nor minimum of the profile appears.

noncomputable def EulerLinearDuhamel.Evolution.weightedSolution {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) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : C(↑(Set.Icc 0 T), E)

The normalized constructed path, with normalized forcing as input.

Equations

• U.weightedSolution g hg f a₀ = (EulerContinuousTimeWeight.normalize g hg) (U.solution ((EulerContinuousTimeWeight.weight g) f) a₀)

theorem EulerLinearDuhamel.Evolution.weightedSolution_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) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : U.weightedSolution g hg f a₀ = (U.weightedInitial g hg) a₀ + (U.weightedForcing g hg) f

The normalized solution is still exactly the two actual data maps.

theorem EulerLinearDuhamel.Evolution.frozen_solution {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) {D : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (V : Evolution T hT D) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : V.solution f a₀ = U.initialOperator a₀ + U.forcingOperator (f + (EulerContinuousTimeIntegral.multiplier (D - B)) (V.solution f a₀))

Freezing the coefficient is an actual identity of constructed solutions.

theorem EulerLinearDuhamel.Evolution.weighted_frozen_solution {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) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) {D : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (V : Evolution T hT D) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : V.weightedSolution g hg f a₀ = (U.weightedInitial g hg) a₀ + (U.weightedForcing g hg) (f + (EulerContinuousTimeIntegral.multiplier (D - B)) (V.weightedSolution g hg f a₀))

The exact frozen identity in the fixed profile-normalized path space.