Same-radius fixed-Sobolev estimates for the actual transverse history

The finite base order stays inside each external word. Only coefficient tensor bounds are converted to word sums; forcing and solution use the same external radius and base order. The recurrence is applied to the actual coercive inverse, with its proved polynomial norm bound.

Uniform factorial estimates for the constructed transverse inverse

Every constant is an explicit polynomial in the interval length, frame bounds, potential bound, and reciprocal frame lower bound. The same radius works at every derivative order and input shift. The recurrence is derived from the actual inverse equation, not assumed for an abstract jet.

Factorial coefficient estimates for the actual transverse form

The coefficient constants below are polynomial in the frame bounds and the interval length. They control genuine Fréchet derivatives of the concrete fixed-space operator and forcing, without a packaged jet or recurrence input.

def EulerTransverseCoefficientGevrey.derivativeCost (T C₀ C₁ : ℝ) : ℝ

The polynomial coefficient cost of taking a physical derivative.

Equations

• EulerTransverseCoefficientGevrey.derivativeCost T C₀ C₁ = T * C₁ + C₀

def EulerTransverseCoefficientGevrey.formCost (T C₀ C₁ CH : ℝ) : ℝ

The polynomial coefficient cost of the transported variational form.

Equations

• EulerTransverseCoefficientGevrey.formCost T C₀ C₁ CH = 9 * EulerTransverseCoefficientGevrey.derivativeCost T C₀ C₁ ^ 2 * (1 + T ^ 2 * CH)

def EulerTransverseCoefficientGevrey.forcingCost (T C₀ C₁ : ℝ) : ℝ

The polynomial cost of the actual weak forcing term.

Equations

• EulerTransverseCoefficientGevrey.forcingCost T C₀ C₁ = 3 * (T * EulerTransverseCoefficientGevrey.derivativeCost T C₀ C₁)

theorem EulerTransverseCoefficientGevrey.fixedFrameDerivative_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (R C₀ C₁ : ℝ) (hR : 0 ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant R 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT (Q y) (Q₁ y)) x‖ ≤ derivativeCost T C₀ C₁ * EulerGevrey.majorant R 0 n

Every actual derivative of the fixed kinetic map has the same factorial bound.

theorem EulerTransverseCoefficientGevrey.fixedFramePrimitive_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (R C₀ C₁ : ℝ) (hR : 0 ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant R 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseFixedSpaceInverse.fixedFramePrimitive T hT (Q y) (Q₁ y)) x‖ ≤ T * derivativeCost T C₀ C₁ * EulerGevrey.majorant R 0 n

Terminal integration adds only the interval-length factor.

theorem EulerTransverseCoefficientGevrey.dirichletOperator_bound {P : Type u_1} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hH : ContDiff ℝ (↑⊤) H) (R CH : ℝ) (hR : 0 ≤ R) (hCH : 0 ≤ CH) (hbH : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseVariationalInverse.dirichletOperator (EulerTerminalTimePrimitive.primitiveTimeLp T hT) (EulerTimeLp.timeMultiplier T hT (H y))) x‖ ≤ (1 + T ^ 2 * CH) * EulerGevrey.majorant R 0 n

The physical Dirichlet form has the coefficient-only factorial bound.

theorem EulerTransverseCoefficientGevrey.fixedFrameOperator_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (R C₀ C₁ CH : ℝ) (hR : 0 ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant R 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (hbH : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseFixedSpaceInverse.fixedFrameOperator T hT (Q y) (Q₁ y) (H y)) x‖ ≤ formCost T C₀ C₁ CH * EulerGevrey.majorant R 0 n

Factorial control of the concrete fixed-space operator follows from the prescribed paths.

theorem EulerTransverseCoefficientGevrey.fixedForcing_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (R C₀ C₁ : ℝ) (hR : 0 ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant R 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (f : P → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (-ContinuousLinearMap.adjoint (EulerTransverseFixedSpaceInverse.fixedFramePrimitive T hT (Q y) (Q₁ y))) (f y)) x‖ ≤ forcingCost T C₀ C₁ * EulerGevrey.majorant R d n

The genuine weak right side has the input shift with a fixed polynomial cost.

noncomputable def EulerTransverseGevreyInverse.transportCeiling (T C₀ C₁ c : ℝ) : ℝ

Uniform polynomial bound for the inverse frame transport.

Equations

• EulerTransverseGevreyInverse.transportCeiling T C₀ C₁ c = 1 + ((2 * c⁻¹ ^ 2 * C₀ ^ 2 * C₁ + c⁻¹ * C₁) * T + c⁻¹ * C₀)

noncomputable def EulerTransverseGevreyInverse.inverseCost (T C₀ C₁ c : ℝ) : ℝ

Uniform polynomial bound for the inverse of the transported form.

Equations

• EulerTransverseGevreyInverse.inverseCost T C₀ C₁ c = 2 * EulerTransverseGevreyInverse.transportCeiling T C₀ C₁ c ^ 2

noncomputable def EulerTransverseGevreyInverse.solveCost (T C₀ C₁ CH c : ℝ) : ℝ

One polynomial top constant handles both coefficient and forcing amplitudes.

Equations

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

theorem EulerTransverseGevreyInverse.fixedCoercivity_inv_le {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (C₀ C₁ : ℝ) (hQ : ‖Q‖ ≤ C₀) (hQ₁ : ‖Q₁‖ ≤ C₁) : (EulerTransverseFixedSpaceInverse.fixedCoercivity T Q Q₁ c)⁻¹ ≤ inverseCost T C₀ C₁ c

The explicit fixed-space coercivity gives the promised polynomial inverse bound.

theorem EulerTransverseGevreyInverse.solveCost_one_le (T C₀ C₁ CH c : ℝ) (hT : 0 ≤ T) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) : 1 ≤ solveCost T C₀ C₁ CH c

The top constant is at least one for all nonnegative coefficient bounds.

theorem EulerTransverseGevreyInverse.fixedFrameSolution_gevrey {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : P) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (R : ℝ) (hR : 2 * solveCost T C₀ C₁ CH c * (Rc + 1) ≤ R) (f : P → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT (Q y) (Q₁ y) (H y) c hc ⋯ ⋯ K hK ⋯ hsmall) (f y)) x‖ ≤ EulerGevrey.majorant R (d + 1) n

The actual zero-endpoint coordinate solve has a single-shift factorial bound with a radius uniform in the derivative order and input shift.

theorem EulerTransverseGevreyInverse.transverseCoordinates_gevrey {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : P) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (m : P → ↑(Set.Icc 0 T) → E) (hTangent : ∀ (y : P) (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (m y t) (((Q y) t) v) = 0) (hRange : ∀ (y : P) (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m y t) η = 0 → ∃ (v : U), ((Q y) t) v = η) (R : ℝ) (hR : 2 * solveCost T C₀ C₁ CH c * (Rc + 1) ≤ R) (f : P → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseCoordinateRegularity.coordinateDerivative T hT (Q y) (Q₁ y) c hc ⋯ ↑((EulerTransverseVariationalInverse.transverseSolver T hT (m y) (H y) K hK ⋯ hsmall) (f y))) x‖ ≤ EulerGevrey.majorant R (d + 1) n

The factorial estimate applies to the recovered coordinate derivative of the original physical transverse solver.

theorem EulerTransverseGevreyInverse.transverseVelocity_gevrey {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : P) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (m : P → ↑(Set.Icc 0 T) → E) (hTangent : ∀ (y : P) (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (m y t) (((Q y) t) v) = 0) (hRange : ∀ (y : P) (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m y t) η = 0 → ∃ (v : U), ((Q y) t) v = η) (R : ℝ) (hR : 2 * solveCost T C₀ C₁ CH c * (Rc + 1) ≤ R) (f : P → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (EulerTimeLp.timeMultiplier T hT (Q y)) (EulerTransverseCoordinateRegularity.coordinateDerivative T hT (Q y) (Q₁ y) c hc ⋯ ↑((EulerTransverseVariationalInverse.transverseSolver T hT (m y) (H y) K hK ⋯ hsmall) (f y)))) x‖ ≤ 3 * C₀ * EulerGevrey.majorant R (d + 1) n

The actual physical transverse velocity has the same factorial shift, with only the fixed coefficient multiplication constant.

def EulerTransverseFixedSobolev.forcingBlockAmplitude (ι : Type u_1) [Fintype ι] (q : ℕ) (T Rc C₀ C₁ Cf : ℝ) : ℝ

Forcing block amplitude, given by 3*sobolevCoefficientAmplitude ι q Rc (T*derivativeCost T C₀ C₁)*Cf.

Equations

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

noncomputable def EulerTransverseFixedSobolev.blockCost (ι : Type u_1) [Fintype ι] (q : ℕ) (T Rc C₀ C₁ CH c Cf : ℝ) : ℝ

Block cost, given by inverseBlockCost ι q (inverseCost T C₀ C₁ c) Rc (formCost T C₀ C₁ CH) (forcingBlockAmplitude ι q T Rc C₀ C₁ Cf).

Equations

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

theorem EulerTransverseFixedSobolev.forcingBlockAmplitude_nonneg (ι : Type u_1) [Fintype ι] (q : ℕ) (T Rc C₀ C₁ Cf : ℝ) (hT : 0 ≤ T) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCf : 0 ≤ Cf) : 0 ≤ forcingBlockAmplitude ι q T Rc C₀ C₁ Cf

theorem EulerTransverseFixedSobolev.blockCost_one_le (ι : Type u_1) [Fintype ι] (q : ℕ) (T Rc C₀ C₁ CH c Cf : ℝ) (hT : 0 ≤ T) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) : 1 ≤ blockCost ι q T Rc C₀ C₁ CH c Cf

theorem EulerTransverseFixedSobolev.forcingOperator_bound {X : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (Rc C₀ C₁ : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hbQ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (x : X) : ‖iteratedFDeriv ℝ n (fun (y : X) => -ContinuousLinearMap.adjoint (EulerTransverseFixedSpaceInverse.fixedFramePrimitive T hT (Q y) (Q₁ y))) x‖ ≤ T * EulerTransverseCoefficientGevrey.derivativeCost T C₀ C₁ * EulerGevrey.majorant Rc 0 n

The actual weak forcing pullback has coefficient-only tensor bounds.

theorem EulerTransverseFixedSobolev.solver_block_gevrey {X : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → X) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH Cf R : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hbQ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hR : 2 * blockCost ι q T Rc C₀ C₁ CH c Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (f : X → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hfb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT (Q y) (Q₁ y) (H y) c hc ⋯ ⋯ K hK ⋯ hsmall) (f y)) n x ≤ EulerGevrey.majorant R (d + 1) n

The genuine zero-trace coordinate solver gains one factorial shift at the identical external radius and fixed base Sobolev order.

theorem EulerTransverseFixedSobolev.velocityLp_block_gevrey {X : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → X) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH Cf R : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hbQ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hR : 2 * blockCost ι q T Rc C₀ C₁ CH c Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (f : X → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hfb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (EulerTransverseFixedEvolution.velocityLp T hT (Q y) (Q₁ y) (H y) c hc ⋯ ⋯ K hK ⋯ hsmall) (f y)) n x ≤ EulerGevrey.majorant R (d + 1) n

Forgetting the zero-trace subtype is a contraction, so the actual coordinate L² velocity has the identical word estimate.