The actual uniform-time Gram inverse in fixed Sobolev word blocks.

theorem EulerContinuousGramSobolev.solution_block_gevrey {P : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (Q : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hQ : ContDiff ℝ (↑⊤) Q) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (f : P → C(↑(Set.Icc 0 T), U)) (hf : ContDiff ℝ (↑⊤) f) (D R : ℝ) (hD : 0 ≤ D) (hR : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C D * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q f n x ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : EulerParameterWordGevrey.block directions q (fun (y : P) => (EulerContinuousGramPath.solve T (Q y) c hc ⋯) (f y)) n x ≤ EulerGevrey.majorant R (d + 1) n

The continuous Gram solve is bounded in the same fixed Sobolev order and external radius as its input, with one factorial shift and a fixed cost.