The literal slow curl as a continuous cylinder L² path with same-radius bounds.

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds1 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds2 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds3 : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds3 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds4 : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds4 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds5 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds5 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds6 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds6 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds7 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds7 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds8 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds8 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds9 (P : ℝ) [Fact (0 < P)] : NormedAddCommGroup ↥(EulerLiftedGradientSpace.LiftL2 P)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds9 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds10 (P : ℝ) [Fact (0 < P)] : NormedSpace ℝ ↥(EulerLiftedGradientSpace.LiftL2 P)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds10 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds11 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedAddCommGroup C(K,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds11 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlBounds12 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedSpace ℝ C(K,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlBounds12 P = inferInstance

theorem EulerCylinderSlowCurl.path_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (q : ℕ) (Rc C R D : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hbG : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath G) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbp : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) n 0 ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (path P G p)) n 0 ≤ 9 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * D * EulerGevrey.majorant R (d + 1) n

One spatial derivative consumes one shift; the external radius is unchanged.