The forward estimate in actual fixed-Sobolev external-word blocks

The normalized Duhamel solution satisfies the constructed frozen equation. Its inverse at the base point is literally Id. Applying the finite base-order inverse estimate and then the external-word recurrence gives one factorial shift at the same input/output radius. Every constant is a fixed polynomial in the coefficient, data, propagator and time-length constants when q is fixed.

Quantitative bounds for the actual frozen forward equation

The frozen coefficient has a polynomial tensor multiplier bound derived from the original coefficient and the H3 Green bound. Its fixed-Sobolev forcing block is bounded directly by the original initial/forcing blocks. No profile extremum, inverse amplitude, or raw weighted primitive is used.

A frozen bounded-operator equation for the actual forward solve

At a chosen parameter x, Duhamel gives an exact equation with coefficient Id minus the fixed Green operator applied to the coefficient difference. Its coefficient at x is exactly Id. Thus the fixed-Sobolev inverse estimate can use the identity inverse; it never requires a norm for a profile-weighted raw time primitive.

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenOperator1 {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.instLinearDuhamelFrozenOperator1 = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenOperator2 {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.instLinearDuhamelFrozenOperator2 = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenOperator3 {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.instLinearDuhamelFrozenOperator3 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenOperator4 {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.instLinearDuhamelFrozenOperator4 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenOperator5 {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.instLinearDuhamelFrozenOperator5 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenOperator6 {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.instLinearDuhamelFrozenOperator6 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenOperator7 {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.instLinearDuhamelFrozenOperator7 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenOperator8 {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.instLinearDuhamelFrozenOperator8 T = inferInstance

noncomputable def EulerLinearDuhamel.frozenOperator {P : Type u_1} {E : Type u_2} [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) (x y : P) : C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), E)

The exact frozen coefficient, using the actual weighted Green operator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerLinearDuhamel.frozenForcing {P : Type u_1} {E : Type u_2} [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) (x y : P) : C(↑(Set.Icc 0 T), E)

The exact transformed data under the fixed homogeneous and Green operators.

Equations

• EulerLinearDuhamel.frozenForcing T hT B U g hg f a₀ x y = ((U x).weightedInitial g hg) (a₀ y) + ((U x).weightedForcing g hg) (f y)

theorem EulerLinearDuhamel.frozenOperator_self {P : Type u_1} {E : Type u_2} [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) (x : P) : frozenOperator T hT B U g hg x x = ContinuousLinearMap.id ℝ C(↑(Set.Icc 0 T), E)

The frozen coefficient at its base parameter is the identity.

theorem EulerLinearDuhamel.frozenOperator_equation {P : Type u_1} {E : Type u_2} [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) (x y : P) : (frozenOperator T hT B U g hg x y) ((U y).weightedSolution g hg (f y) (a₀ y)) = frozenForcing T hT B U g hg f a₀ x y

The actual normalized Duhamel solution satisfies this bounded-operator equation.

theorem EulerLinearDuhamel.frozenOperator_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) (hB : ContDiff ℝ (↑⊤) B) (x : P) : ContDiff ℝ (↑⊤) (frozenOperator T hT B U g hg x)

The frozen coefficient is genuinely smooth in the translated coefficients.

theorem EulerLinearDuhamel.frozenForcing_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) (hf : ContDiff ℝ (↑⊤) f) (ha₀ : ContDiff ℝ (↑⊤) a₀) (x : P) : ContDiff ℝ (↑⊤) (frozenForcing T hT B U g hg f a₀ x)

The transformed data retain the actual parameter smoothness of the original data.

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenGevrey1 {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.instLinearDuhamelFrozenGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenGevrey2 {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.instLinearDuhamelFrozenGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenGevrey3 {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.instLinearDuhamelFrozenGevrey3 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenGevrey4 {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.instLinearDuhamelFrozenGevrey4 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenGevrey5 {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.instLinearDuhamelFrozenGevrey5 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenGevrey6 {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.instLinearDuhamelFrozenGevrey6 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenGevrey7 {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.instLinearDuhamelFrozenGevrey7 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelFrozenGevrey8 {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.instLinearDuhamelFrozenGevrey8 T = inferInstance

def EulerLinearDuhamel.frozenAmplitude (T C CB : ℝ) : ℝ

The frozen coefficient amplitude is polynomial in the original coefficient and H3 constant.

Equations

• EulerLinearDuhamel.frozenAmplitude T C CB = 1 + 2 * C * T * CB

theorem EulerLinearDuhamel.frozenOperator_bound {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) (hB : ContDiff ℝ (↑⊤) B) (hg₀ : g ⟨0, ⋯⟩ = 1) (C CB Rc : ℝ) (hC : 0 ≤ C) (hCB : 0 ≤ CB) (hRc : 0 ≤ Rc) (hBb : ∀ (n : ℕ) (y : P), ‖iteratedFDeriv ℝ n B y‖ ≤ CB * EulerGevrey.majorant Rc 0 n) (x : P) (hU : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ‖(U x).propagator t s‖ ≤ C * g t / g s) (n : ℕ) (y : P) : ‖iteratedFDeriv ℝ n (frozenOperator T hT B U g hg x) y‖ ≤ frozenAmplitude T C CB * EulerGevrey.majorant Rc 0 n

Actual derivatives of the frozen coefficient have the stated polynomial bound.

theorem EulerLinearDuhamel.frozenForcing_block_bound {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) {ι : Type u_3} [Fintype ι] (directions : ι → P) (q : ℕ) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → E) (hf : ContDiff ℝ (↑⊤) f) (ha₀ : ContDiff ℝ (↑⊤) a₀) (hg₀ : g ⟨0, ⋯⟩ = 1) (C A D R : ℝ) (hC : 0 ≤ C) (x : P) (hU : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ‖(U x).propagator t s‖ ≤ C * g t / g s) (d : ℕ) (hfa : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q f n x ≤ D * EulerGevrey.majorant R d n) (haa : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q a₀ n x ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (frozenForcing T hT B U g hg f a₀ x) n x ≤ (C * A + C * T * D) * EulerGevrey.majorant R d n

The transformed right side preserves the original fixed-Sobolev external radius.

The fixed-Sobolev inverse estimate needs bounds only at its base point

In particular a frozen Duhamel equation has identity as its base operator. The actual equation and smoothness hold as functions; every quantitative hypothesis, including invertibility, is needed only at the evaluation point.

theorem EulerParameterWordGevrey.block_inverse_gevrey_at {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (A : P → E →L[ℝ] E) (u f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (heq : ∀ (y : P), (A y) (u y) = f y) (x : P) (inverse : E →L[ℝ] E) (hleft : ∀ (v : E), inverse ((A x) v) = v) (I B C D M Rc R : ℝ) (_hC : 0 ≤ C) (_hD : 0 ≤ D) (hM : 1 ≤ M) (hMC : sobolevInverseCost I B q * C ≤ M) (hMD : sobolevInverseCost I B q * D ≤ M) (hRc : 0 ≤ Rc) (hR : 2 * M * (Rc + 1) ≤ R) (hinv : ‖inverse‖ ≤ I) (hbase : baseSize directions q A x ≤ B) (hcoeff : ∀ (j : ℕ), coefficientBlock directions q A (j + 1) x ≤ C * (Rc ^ (j + 1) * ↑(j + 1).factorial ^ 2)) (d : ℕ) (hforce : ∀ (n : ℕ), block directions q f n x ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : block directions q u n x ≤ EulerGevrey.majorant R (d + 1) n

def EulerLinearDuhamel.forwardSobolevAmplitude (ι : Type u_1) [Fintype ι] (q : ℕ) (T C CB Rc : ℝ) : ℝ

The once-enlarged coefficient amplitude for the frozen equation at fixed base order.

Equations

• EulerLinearDuhamel.forwardSobolevAmplitude ι q T C CB Rc = EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc (EulerLinearDuhamel.frozenAmplitude T C CB)

def EulerLinearDuhamel.forwardSobolevCost (ι : Type u_1) [Fintype ι] (q : ℕ) (T C A D CB Rc : ℝ) : ℝ

A fixed polynomial cost for the source's forward Hq external-word estimate.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelSobolevGevrey1 {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.instLinearDuhamelSobolevGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelSobolevGevrey2 {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.instLinearDuhamelSobolevGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelSobolevGevrey3 {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.instLinearDuhamelSobolevGevrey3 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelSobolevGevrey4 {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.instLinearDuhamelSobolevGevrey4 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelSobolevGevrey5 {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.instLinearDuhamelSobolevGevrey5 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelSobolevGevrey6 {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.instLinearDuhamelSobolevGevrey6 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelSobolevGevrey7 {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.instLinearDuhamelSobolevGevrey7 T = inferInstance

@[instance_reducible]

noncomputable def EulerLinearDuhamel.instLinearDuhamelSobolevGevrey8 {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.instLinearDuhamelSobolevGevrey8 T = inferInstance

theorem EulerLinearDuhamel.weightedSolution_block_gevrey_at {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (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 * forwardSobolevCost ι q T C A D CB Rc * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hBb : ∀ (n : ℕ) (y : P), ‖iteratedFDeriv ℝ n B y‖ ≤ CB * EulerGevrey.majorant Rc 0 n) (x : P) (hU : ∀ (t s : ↑(Set.Icc 0 T)), s ≤ t → ‖(U x).propagator t s‖ ≤ C * g t / g s) (d : ℕ) (hforce : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q f n x ≤ D * EulerGevrey.majorant R d n) (hinitial : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q a₀ n x ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (y : P) => (U y).weightedSolution g hg (f y) (a₀ y)) n x ≤ EulerGevrey.majorant R (d + 1) n

The actual fixed-Hq block of the forward solution gains just one shift, with an unchanged radius and with H3 used only at the base parameter.