Actual within-time differentiation and bounds for the constructed slow-curl path.

noncomputable def EulerCylinderSlowCurl.derivative (P : ℝ) [Fact (0 < P)] (T : ℝ) (G G₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Derivative, given by path P G₁ p + path P G f.

Equations

• EulerCylinderSlowCurl.derivative P T G G₁ p f = EulerCylinderSlowCurl.path P G₁ p + EulerCylinderSlowCurl.path P G f

theorem EulerCylinderSlowCurl.derivative_orbit (P : ℝ) [Fact (0 < P)] (T : ℝ) (G G₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (hG₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G₁)) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (derivative P T G G₁ p f)

@[instance_reducible]

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

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlTime1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlTime2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlTime3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlTime4 = inferInstance

theorem EulerCylinderSlowCurl.path_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (G G₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hGt : ∀ t ∈ Set.Icc 0 T, ∀ (y : EulerSmoothLimit.Space), HasDerivWithinAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath T hT G r) y) ((EulerVolterraConvolution.extendPath T hT G₁ t) y) (Set.Icc 0 T) t) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (f t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (path P G p)) ((derivative P T G G₁ p f) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderSlowCurl.field_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (G G₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (hG₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G₁)) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hGt : ∀ t ∈ Set.Icc 0 T, ∀ (y : EulerSmoothLimit.Space), HasDerivWithinAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath T hT G r) y) ((EulerVolterraConvolution.extendPath T hT G₁ t) y) (Set.Icc 0 T) t) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (f t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : HasDerivWithinAt (fun (r : ℝ) => field P G hG p hp (Set.projIcc 0 T hT r) x) (EulerCylinderSmoothOrbit.pointField P (derivative P T G G₁ p f) ⋯ t x) (Set.Icc 0 T) ↑t

The reconstructed classical curl has the derivative of the actual L² construction.

theorem EulerCylinderSlowCurl.derivative_block_bound (P : ℝ) [Fact (0 < P)] (T : ℝ) (G G₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (hG₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G₁)) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (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) (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) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (derivative P T G G₁ p f)) n 0 ≤ 18 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * D * EulerGevrey.majorant R (d + 1) n

The true curl time derivative retains the same radius and one spatial shift.