The forced initial value problem from a homogeneous evolution

The source assumes a bound for the homogeneous tangent propagator. Here a homogeneous fundamental evolution is the input; the forced path is an actual Bochner integral. Its differential equation, initial trace, uniqueness, and weighted bounds are proved, rather than included in the evolution data.

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

A homogeneous fundamental evolution, with its actual inverse. This data contains no forced solution or estimate for one.

• forward : C(↑(Set.Icc 0 T), E →L[ℝ] E)

  Forward of Evolution, of type C(Icc (0 : ℝ) T,E →L[ℝ] E).

• backward : C(↑(Set.Icc 0 T), E →L[ℝ] E)

  Backward of Evolution, of type C(Icc (0 : ℝ) T,E →L[ℝ] E).

• forward_backward (t : ↑(Set.Icc 0 T)) : self.forward t ∘SL self.backward t = ContinuousLinearMap.id ℝ E
• backward_forward (t : ↑(Set.Icc 0 T)) : self.backward t ∘SL self.forward t = ContinuousLinearMap.id ℝ E
• derivative (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT self.forward) (B t ∘SL self.forward t) (Set.Icc 0 T) ↑t

def EulerLinearDuhamel.Evolution.unit {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) (t : ↑(Set.Icc 0 T)) : (E →L[ℝ] E)ˣ

The algebraic unit represented by the homogeneous fundamental map.

Equations

• U.unit t = { val := U.forward t, inv := U.backward t, val_inv := ⋯, inv_val := ⋯ }

theorem EulerLinearDuhamel.Evolution.backward_eq_inverse {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) (t : ↑(Set.Icc 0 T)) : U.backward t = Ring.inverse (U.forward t)

The supplied inverse is the genuine ring inverse.

theorem EulerLinearDuhamel.Evolution.backward_derivative {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) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT U.backward) (-U.backward t ∘SL B t) (Set.Icc 0 T) ↑t

The inverse fundamental map's derivative follows from the inverse theorem.

def EulerLinearDuhamel.Evolution.propagator {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) (t s : ↑(Set.Icc 0 T)) : E →L[ℝ] E

The two-time homogeneous propagator.

Equations

• U.propagator t s = U.forward t ∘SL U.backward s

@[simp]

theorem EulerLinearDuhamel.Evolution.propagator_self {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) (t : ↑(Set.Icc 0 T)) : U.propagator t t = ContinuousLinearMap.id ℝ E

A propagator starts at the identity.

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

The forcing pulled back by the inverse homogeneous evolution.

Equations

• U.transformedForcing f s = (EulerVolterraConvolution.extendPath T hT U.backward s) (EulerVolterraConvolution.extendPath T hT f s)

theorem EulerLinearDuhamel.Evolution.transformedForcing_continuous {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) (f : C(↑(Set.Icc 0 T), E)) : Continuous (U.transformedForcing f)

The pulled-back forcing is genuinely continuous.

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

Duhamel's formula, as an actual interval integral.

Equations

• U.solutionReal f a₀ t = (EulerVolterraConvolution.extendPath T hT U.forward t) ((U.backward ⟨0, ⋯⟩) a₀ + ∫ (s : ℝ) in 0..t, U.transformedForcing f s)

theorem EulerLinearDuhamel.Evolution.solutionReal_continuous {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) : Continuous (U.solutionReal f a₀)

The constructed forced path is continuous.

noncomputable def EulerLinearDuhamel.Evolution.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) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : C(↑(Set.Icc 0 T), E)

The actual continuous forced solution on the time interval.

Equations

• U.solution f a₀ = { toFun := fun (t : ↑(Set.Icc 0 T)) => U.solutionReal f a₀ ↑t, continuous_toFun := ⋯ }

@[simp]

theorem EulerLinearDuhamel.Evolution.solution_initial {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₀) ⟨0, ⋯⟩ = a₀

Duhamel's formula attains the prescribed initial data.

theorem EulerLinearDuhamel.Evolution.solution_derivative {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) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (U.solutionReal f a₀) ((B t) ((U.solution f a₀) t) + f t) (Set.Icc 0 T) ↑t

The actual constructed path solves the inhomogeneous differential equation.

theorem EulerLinearDuhamel.Evolution.solution_duhamel {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) (t : ↑(Set.Icc 0 T)) : (U.solution f a₀) t = (U.propagator t ⟨0, ⋯⟩) a₀ + ∫ (s : ℝ) in 0..↑t, (U.forward t) (U.transformedForcing f s)

The same solution has the literal two-time Duhamel formula.

theorem EulerLinearDuhamel.Evolution.solution_unique {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) (a : ℝ → E) (ha : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt a ((B t) (a ↑t) + f t) (Set.Icc 0 T) ↑t) (h₀ : a 0 = a₀) (t : ↑(Set.Icc 0 T)) : a ↑t = (U.solution f a₀) t

Any differentiable path with the same forcing and initial data equals the actual integral construction. No uniqueness assertion is assumed of the data.

theorem EulerLinearDuhamel.Evolution.solution_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)) (a₀ : 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.solution f a₀) t‖ ≤ C * g t * (‖a₀‖ + ↑t * D)

A relative homogeneous propagator bound yields the forced bound with the same profile. No exponential in the coefficient norm is introduced.