Genuine fixed-Sobolev bounds for the cylinder history inverse

The actual mixed translation orbit has identical fixed-base word norms at every translation. Thus the forcing needs a bound only at zero. Coefficient jets lift to L² operator paths with constant one, and the true fixed-space inverse adds one shift while preserving the external radius.

Actual mixed coefficient jets in the uniform-time L² operator norm.

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds1 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (E →L[ℝ] F)

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

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds2 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (E →L[ℝ] F)

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

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds3 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds3 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds4 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds4 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds5 {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

Cache the standard NormedAddCommGroup C(K,Space →ᵇ E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds5 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds6 {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

Cache the standard NormedSpace ℝ C(K,Space →ᵇ E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds6 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds7 (P : ℝ) [Fact (0 < P)] {E : Type u_1} [NormedAddCommGroup E] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 P E)

Cache the standard NormedAddCommGroup (CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds7 P = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds8 (P : ℝ) [Fact (0 < P)] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 P E)

Cache the standard NormedSpace ℝ (CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds8 P = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds9 (P : ℝ) [Fact (0 < P)] {F : Type u_2} [NormedAddCommGroup F] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 P F)

Cache the standard NormedAddCommGroup (CylinderL2 P F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds9 P = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds10 (P : ℝ) [Fact (0 < P)] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 P F)

Cache the standard NormedSpace ℝ (CylinderL2 P F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds10 P = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds11 (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds11 P = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds12 (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds12 P = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds13 (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))

Cache the standard NormedAddCommGroup C(K,CylinderL2 P E →L[ℝ] CylinderL2 P F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds13 P = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderPathBounds14 (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))

Cache the standard NormedSpace ℝ C(K,CylinderL2 P E →L[ℝ] CylinderL2 P F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderPathBounds14 P = inferInstance

noncomputable def EulerLpCylinderRectangular.mixedOperatorPath (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (a : EulerLiftedGradientSpace.LiftTangent) : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))

Mixed operator path, given by fullPathMap P (translateCoefficientPath A a.1).

Equations

• EulerLpCylinderRectangular.mixedOperatorPath P A a = (EulerLpCylinderRectangular.fullPathMap P) (EulerMeanCoefficients.translateCoefficientPath A a.1)

theorem EulerLpCylinderRectangular.mixedOperatorPath_contDiff (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) : ContDiff ℝ (↑⊤) (mixedOperatorPath P A)

theorem EulerLpCylinderRectangular.mixedOperatorPath_bound (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (n : ℕ) (C : ℝ) (hb : ∀ (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) a‖ ≤ C) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (mixedOperatorPath P A) a‖ ≤ C

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev1 (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 P U)

Cache the standard NormedAddCommGroup (CylinderL2 P U) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev1 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev2 (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 P U)

Cache the standard NormedSpace ℝ (CylinderL2 P U) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev3 (P : ℝ) [Fact (0 < P)] {E : Type u_2} [NormedAddCommGroup E] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 P E)

Cache the standard NormedAddCommGroup (CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev3 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev4 (P : ℝ) [Fact (0 < P)] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 P E)

Cache the standard NormedSpace ℝ (CylinderL2 P E) instance to shorten typeclass synthesis.

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev4 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev5 (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev5 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev6 (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev6 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev7 (P : ℝ) [Fact (0 < P)] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev7 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev8 (P : ℝ) [Fact (0 < P)] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev8 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev9 (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev9 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev10 (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev10 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev11 (P : ℝ) [Fact (0 < P)] {T : ℝ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev11 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev12 (P : ℝ) [Fact (0 < P)] {T : ℝ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

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

Equations

• EulerCylinderDirichlet.Coefficients.instCylinderDirichletSobolev12 P = inferInstance

theorem EulerCylinderDirichlet.Coefficients.frameOrbit_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q)) (n : ℕ) (C : ℝ) (hb : ∀ (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ C) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => frame P (D.shifted b.1)) a‖ ≤ C

theorem EulerCylinderDirichlet.Coefficients.frameDerivativeOrbit_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁)) (n : ℕ) (C : ℝ) (hb : ∀ (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ C) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => frameDerivative P (D.shifted b.1)) a‖ ≤ C

theorem EulerCylinderDirichlet.Coefficients.hessianOrbit_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H)) (n : ℕ) (C : ℝ) (hb : ∀ (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ C) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => hessian P (D.shifted b.1)) a‖ ≤ C

theorem EulerCylinderDirichlet.Coefficients.velocityLp_block_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) {ι : Type u_3} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q)) (hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁)) (hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H)) (Rc C₀ C₁ CH Cf R : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hbQ : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hR : 2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH D.lower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f) (d : ℕ) (hfb : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap) f) n 0 ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P b).toContinuousLinearMap) ((velocityLp P D) f)) n a ≤ EulerGevrey.majorant R (d + 1) n

Actual cylinder/time L² coordinate velocity: one shift at the original radius and fixed Sobolev order, from forcing bounds at the base translation.

theorem EulerCylinderDirichlet.Coefficients.continuous_velocityLp_block_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) {ι : Type u_3} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q)) (hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁)) (hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H)) (Rc C₀ C₁ CH Cf R : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hbQ : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hR : 2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH D.lower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hT1 : T ≤ 1) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (d : ℕ) (hfb : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerTimeLpBoundedMap.timeLift T (EulerLpCylinderTranslation.translate P b).toContinuousLinearMap) ((velocityLp P D) (EulerTimeLp.pathLp T ⋯ f))) n a ≤ EulerGevrey.majorant R (d + 1) n

For source intervals of length at most one, continuous forcing embeds with no extra amplitude, and the same history estimate applies.