Genuine time derivatives of the constructed vector potential and its slow curl.

Actual one-sided time differentiation of the packet's spatial curl corrector.

theorem EulerPacketPiola.matrixSlowCurl_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (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) (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) (G : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (G₁ : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hG : HasDerivWithinAt G G₁ (Set.Icc 0 T) ↑t) : HasDerivWithinAt (fun (r : ℝ) => EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P p hp (Set.projIcc 0 T hT r)) x ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G r)) (EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P f hf t) x ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G ↑t) + EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P p hp t) x ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G₁)) (Set.Icc 0 T) ↑t

The two product-rule terms are derived from the genuine L² evolution and actual inverse frame derivative.

theorem EulerPacketPiola.liftedSlowCurl_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (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) (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) (F : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (G₁ : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hG : HasDerivWithinAt (fun (r : ℝ) => ↑(F r x.1).symm) G₁ (Set.Icc 0 T) ↑t) : HasDerivWithinAt (fun (r : ℝ) => liftedSlowCurl P (F r) (EulerCylinderSmoothOrbit.pointField P p hp (Set.projIcc 0 T hT r)) x) (liftedSlowCurl P (F ↑t) (EulerCylinderSmoothOrbit.pointField P f hf t) x + EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P p hp t) x ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G₁)) (Set.Icc 0 T) ↑t

This is the literal lifted curl in the Piola packet construction, including both time endpoints.

noncomputable def EulerCylinderPotential.potentialDerivative (P : ℝ) [Fact (0 < P)] (T : ℝ) (B B₁ : 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))

Potential derivative, given by potentialPath P B₁ p + potentialPath P B f.

Equations

• EulerCylinderPotential.potentialDerivative P T B B₁ p f = EulerCylinderPotential.potentialPath P B₁ p + EulerCylinderPotential.potentialPath P B f

theorem EulerCylinderPotential.potentialDerivative_orbit (P : ℝ) [Fact (0 < P)] (T : ℝ) (B B₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (hB₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B₁)) (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) (potentialDerivative P T B B₁ p f)

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialTime1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderPotential.instCylinderPotentialTime1 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialTime2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderPotential.instCylinderPotentialTime2 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialTime3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderPotential.instCylinderPotentialTime3 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialTime4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderPotential.instCylinderPotentialTime4 = inferInstance

theorem EulerCylinderPotential.potentialPath_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (B B₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hBt : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT B s) x) ((EulerVolterraConvolution.extendPath T hT B₁ t) x) (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 (potentialPath P B p)) ((potentialDerivative P T B B₁ p f) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderPotential.potentialField_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (B B₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (hB₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B₁)) (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) (hBt : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT B s) x) ((EulerVolterraConvolution.extendPath T hT B₁ t) x) (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 : ℝ) => potentialField P B hB p hp (Set.projIcc 0 T hT r) x) (EulerCylinderSmoothOrbit.pointField P (potentialDerivative P T B B₁ p f) ⋯ t x) (Set.Icc 0 T) ↑t

theorem EulerCylinderPotential.potentialCurl_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (T : ℝ) (hT : 0 ≤ T) (B B₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (hB₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B₁)) (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) (hBt : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT B s) x) ((EulerVolterraConvolution.extendPath T hT B₁ t) x) (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) (F : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (G₁ : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hG : HasDerivWithinAt (fun (r : ℝ) => ↑(F r x.1).symm) G₁ (Set.Icc 0 T) ↑t) : HasDerivWithinAt (fun (r : ℝ) => EulerPacketPiola.liftedSlowCurl P (F r) (potentialField P B hB p hp (Set.projIcc 0 T hT r)) x) (EulerPacketPiola.liftedSlowCurl P (F ↑t) (EulerCylinderSmoothOrbit.pointField P (potentialDerivative P T B B₁ p f) ⋯ t) x + EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (potentialField P B hB p hp t) x ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G₁)) (Set.Icc 0 T) ↑t

The actual curl derivative is obtained from the constructed potential, not assumed as a profile jet.