Actual all-order profile estimates for the forward initial value problem

Qualitative smoothness comes from the actual fixed-space Volterra inverse. Quantitative differentiation instead freezes the evolution and uses its profile-normalized Green operator, whose norm is bounded by C*T directly. The profile's extrema never enter the factorial radius or amplitude.

Differentiating a genuine frozen-evolution identity

This calculus lemma applies to actual bounded initial-data and Green operators. The coefficient difference vanishes at the base point, so the resulting binomial recurrence contains only lower solution derivatives on the right.

theorem EulerFrozenEvolutionGevrey.derivative_recurrence {P : Type u_1} {E : Type u_2} {X : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup X] [NormedSpace ℝ X] (B : P → X →L[ℝ] X) (u f : P → X) (a : P → E) (hB : ContDiff ℝ (↑⊤) B) (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (ha : ContDiff ℝ (↑⊤) a) (x : P) (H : E →L[ℝ] X) (K : X →L[ℝ] X) (heq : ∀ (y : P), u y = H (a y) + K (f y + (B y - B x) (u y))) (n : ℕ) : ‖iteratedFDeriv ℝ n u x‖ ≤ ‖H‖ * ‖iteratedFDeriv ℝ n a x‖ + ‖K‖ * (‖iteratedFDeriv ℝ n f x‖ + ∑ j ∈ Finset.range n, ↑(n.choose (j + 1)) * ‖iteratedFDeriv ℝ (j + 1) B x‖ * ‖iteratedFDeriv ℝ (n - (j + 1)) u x‖)

The triangular recurrence is derived from actual Fréchet derivatives of the frozen equation; it is not an assumed sequence estimate.

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelGevrey1 {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] E)

Cache the standard NormedAddCommGroup (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerLinearDuhamel.instLinearDuhamelGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelGevrey2 {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] E)

Cache the standard NormedSpace ℝ (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerLinearDuhamel.instLinearDuhamelGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelGevrey3 {E : Type u_2} [NormedAddCommGroup E] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), E)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,E) instance to shorten typeclass synthesis.

Equations

• EulerLinearDuhamel.instLinearDuhamelGevrey3 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelGevrey4 {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), E)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,E) instance to shorten typeclass synthesis.

Equations

• EulerLinearDuhamel.instLinearDuhamelGevrey4 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelGevrey5 {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), E →L[ℝ] E)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerLinearDuhamel.instLinearDuhamelGevrey5 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelGevrey6 {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), E →L[ℝ] E)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerLinearDuhamel.instLinearDuhamelGevrey6 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelGevrey7 {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) : NormedAddCommGroup (C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), E))

Cache the standard NormedAddCommGroup (C(Icc (0 : ℝ) T,E) →L[ℝ] C(Icc (0 : ℝ) T,E)) instance to shorten typeclass synthesis.

Equations

• EulerLinearDuhamel.instLinearDuhamelGevrey7 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelGevrey8 {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) : NormedSpace ℝ (C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), E))

Cache the standard NormedSpace ℝ (C(Icc (0 : ℝ) T,E) →L[ℝ] C(Icc (0 : ℝ) T,E)) instance to shorten typeclass synthesis.

Equations

• EulerLinearDuhamel.instLinearDuhamelGevrey8 T = inferInstance

theorem EulerLinearDuhamel.weightedSolution_contDiff {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (B : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (U : (x : P) → Evolution T hT (B x)) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (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).weightedSolution g hg (f x) (a₀ x)

Normalization by a fixed profile preserves actual parameter regularity.

theorem EulerLinearDuhamel.weightedSolution_derivative_recurrence {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (B : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (U : (x : P) → Evolution T hT (B x)) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → E) (hB : ContDiff ℝ (↑⊤) B) (hf : ContDiff ℝ (↑⊤) f) (ha₀ : ContDiff ℝ (↑⊤) a₀) (hg₀ : g ⟨0, ⋯⟩ = 1) (C : ℝ) (hC : 0 ≤ C) (hU : ∀ (x : P) (t s : ↑(Set.Icc 0 T)), s ≤ t → ‖(U x).propagator t s‖ ≤ C * g t / g s) (x : P) (n : ℕ) : ‖iteratedFDeriv ℝ n (fun (y : P) => (U y).weightedSolution g hg (f y) (a₀ y)) x‖ ≤ C * ‖iteratedFDeriv ℝ n a₀ x‖ + C * T * (‖iteratedFDeriv ℝ n f x‖ + ∑ j ∈ Finset.range n, ↑(n.choose (j + 1)) * ‖iteratedFDeriv ℝ (j + 1) (fun (y : P) => EulerContinuousTimeIntegral.multiplier (B y)) x‖ * ‖iteratedFDeriv ℝ (n - (j + 1)) (fun (y : P) => (U y).weightedSolution g hg (f y) (a₀ y)) x‖)

The exact differentiated ODE yields a triangular estimate in the fixed profile norm, with the same homogeneous and Green operators at every order.

def EulerLinearDuhamel.forwardCost (T C A D CB : ℝ) : ℝ

The fixed polynomial amplitude controlling the differentiated forward solve.

Equations

• EulerLinearDuhamel.forwardCost T C A D CB = 1 + C * A + C * T * (D + CB)

theorem EulerLinearDuhamel.weightedSolution_gevrey {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (B : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (U : (x : P) → Evolution T hT (B x)) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → E) (hB : ContDiff ℝ (↑⊤) B) (hf : ContDiff ℝ (↑⊤) f) (ha₀ : ContDiff ℝ (↑⊤) a₀) (hg₀ : g ⟨0, ⋯⟩ = 1) (C A D CB Rc R : ℝ) (hC : 0 ≤ C) (hA : 0 ≤ A) (hD : 0 ≤ D) (hCB : 0 ≤ CB) (hRc : 0 ≤ Rc) (hR : 2 * forwardCost T C A D CB * (Rc + 1) ≤ R) (hU : ∀ (x : P) (t s : ↑(Set.Icc 0 T)), s ≤ t → ‖(U x).propagator t s‖ ≤ C * g t / g s) (hcoeff : ∀ (j : ℕ) (x : P), ‖iteratedFDeriv ℝ (j + 1) B x‖ ≤ CB * (Rc ^ (j + 1) * ↑(j + 1).factorial ^ 2)) (d : ℕ) (hforce : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ D * EulerGevrey.majorant R d n) (hinitial : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n a₀ x‖ ≤ A * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (U y).weightedSolution g hg (f y) (a₀ y)) x‖ ≤ EulerGevrey.majorant R (d + 1) n

The actual forward solve loses one factorial shift. Its radius condition contains only the propagator, coefficient and data amplitudes, and time length.