The potential and slow curl of the actual transverse solution, with their genuine time derivatives.

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCorrector1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCorrector1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCorrector2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCorrector2 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCorrector3 : NormedAddCommGroup EulerSourcePotentialCoefficient.PotentialField

Cache the standard NormedAddCommGroup PotentialField instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCorrector3 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCorrector4 : NormedSpace ℝ EulerSourcePotentialCoefficient.PotentialField

Cache the standard NormedSpace ℝ PotentialField instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCorrector4 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCorrector5 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedAddCommGroup C(↑(Set.Icc 0 D.T), EulerSourcePotentialCoefficient.PotentialField)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) D.T,PotentialField) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketCorrector5 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCorrector6 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedSpace ℝ C(↑(Set.Icc 0 D.T), EulerSourcePotentialCoefficient.PotentialField)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) D.T,PotentialField) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketCorrector6 = inferInstance

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Data.potentialCoefficientPath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : C(↑(Set.Icc 0 D.T), EulerSourcePotentialCoefficient.PotentialField)

Potential coefficient path: an abbreviation for potentialCoefficient D.normal D.normalLower D.normalLower_pos D.normal_lower.

Equations

• D.potentialCoefficientPath = EulerSourcePotentialCoefficient.potentialCoefficient D.normal D.normalLower ⋯ ⋯

theorem EulerTransversePacketProvider.Data.potentialCoefficientPath_orbit {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath)

theorem EulerTransversePacketProvider.Data.potentialCoefficientPath_time {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ℝ) (ht : t ∈ Set.Icc 0 D.T) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ D.potentialCoefficientPath r) x) ((EulerVolterraConvolution.extendPath D.T ⋯ D.potentialDerivative t) x) (Set.Icc 0 D.T) t

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Forcing.instTransversePacketCorrector7 {P : ℝ} [Fact (0 < P)] : NormedAddCommGroup ↥(EulerLiftedGradientSpace.LiftL2 P)

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

Equations

• EulerTransversePacketProvider.Forcing.instTransversePacketCorrector7 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Forcing.instTransversePacketCorrector8 {P : ℝ} [Fact (0 < P)] : NormedSpace ℝ ↥(EulerLiftedGradientSpace.LiftL2 P)

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

Equations

• EulerTransversePacketProvider.Forcing.instTransversePacketCorrector8 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Forcing.instTransversePacketCorrector9 {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯)

Cache the standard NormedAddCommGroup (Supported P Space D.support D.support_measurable) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Forcing.instTransversePacketCorrector9 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Forcing.instTransversePacketCorrector10 {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯)

Cache the standard NormedSpace ℝ (Supported P Space D.support D.support_measurable) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Forcing.instTransversePacketCorrector10 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Forcing.instTransversePacketCorrector11 {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} : NormedAddCommGroup C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) D.T,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Forcing.instTransversePacketCorrector11 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Forcing.instTransversePacketCorrector12 {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} : NormedSpace ℝ C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) D.T,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Forcing.instTransversePacketCorrector12 = inferInstance

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Forcing.fullVelocityPath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))

Full velocity path: an abbreviation for includePath P D.support D.support_measurable (G.velocityPath I).

Equations

• G.fullVelocityPath I = (EulerLpCylinderPaths.includePath P D.support ⋯) (G.velocityPath I)

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Forcing.fullDerivativePath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLpCylinderTranslation.CylinderL2 P EulerSmoothLimit.Space))

Full derivative path: an abbreviation for includePath P D.support D.support_measurable (G.derivativePath I).

Equations

• G.fullDerivativePath I = (EulerLpCylinderPaths.includePath P D.support ⋯) (G.derivativePath I)

theorem EulerTransversePacketProvider.Forcing.fullVelocityPath_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (G.fullVelocityPath I)) ((G.fullDerivativePath I) t) (Set.Icc 0 D.T) ↑t

noncomputable def EulerTransversePacketProvider.Forcing.potentialPath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Potential path, given by EulerCylinderPotential.potentialPath P D.potentialCoefficientPath (G.fullVelocityPath I).

Equations

• G.potentialPath I = EulerCylinderPotential.potentialPath P D.potentialCoefficientPath (G.fullVelocityPath I)

noncomputable def EulerTransversePacketProvider.Forcing.potentialTimePath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Potential time path, constructed using EulerCylinderPotential.potentialDerivative.

Equations

• G.potentialTimePath I = EulerCylinderPotential.potentialDerivative P D.T D.potentialCoefficientPath D.potentialDerivative (G.fullVelocityPath I) (G.fullDerivativePath I)

theorem EulerTransversePacketProvider.Forcing.potentialPath_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (G.potentialPath I)

theorem EulerTransversePacketProvider.Forcing.potentialTimePath_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (G.potentialTimePath I)

theorem EulerTransversePacketProvider.Forcing.potentialPath_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (G.potentialPath I)) ((G.potentialTimePath I) t) (Set.Icc 0 D.T) ↑t

noncomputable def EulerTransversePacketProvider.Forcing.correctorPath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Corrector path, given by EulerCylinderSlowCurl.path P D.FInv.field (G.potentialPath I).

Equations

• G.correctorPath I = EulerCylinderSlowCurl.path P D.FInv.field (G.potentialPath I)

noncomputable def EulerTransversePacketProvider.Forcing.correctorTimePath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Corrector time path, given by EulerCylinderSlowCurl.derivative P D.T D.FInv.field D.inverseDerivative (G.potentialPath I) (G.potentialTimePath I).

Equations

• G.correctorTimePath I = EulerCylinderSlowCurl.derivative P D.T D.FInv.field D.inverseDerivative (G.potentialPath I) (G.potentialTimePath I)

theorem EulerTransversePacketProvider.Forcing.correctorPath_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (G.correctorPath I)

theorem EulerTransversePacketProvider.Forcing.correctorTimePath_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (G.correctorTimePath I)

theorem EulerTransversePacketProvider.Forcing.correctorPath_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (G.correctorPath I)) ((G.correctorTimePath I) t) (Set.Icc 0 D.T) ↑t

noncomputable def EulerTransversePacketProvider.Forcing.corrector {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : EulerPacketProfileRecursion.VectorField

Corrector, defined pointwise by pointField P (G.correctorPath I) (G.correctorPath_orbit I) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• G.corrector I z = EulerCylinderSmoothOrbit.pointField P (G.correctorPath I) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketProvider.Forcing.correctorDerivative {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) : EulerPacketProfileRecursion.VectorField

Corrector derivative, defined pointwise by pointField P (G.correctorTimePath I) (G.correctorTimePath_orbit I) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• G.correctorDerivative I z = EulerCylinderSmoothOrbit.pointField P (G.correctorTimePath I) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

theorem EulerTransversePacketProvider.Forcing.corrector_hasDerivWithinAt {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivWithinAt (fun (r : ℝ) => G.corrector I (r, x, θ)) (G.correctorDerivative I (↑t, x, θ)) (Set.Icc 0 D.T) ↑t

theorem EulerTransversePacketProvider.Forcing.fullVelocityPath_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P (G.fullVelocityPath I) ⋯ t (x, ↑θ) = 0

theorem EulerTransversePacketProvider.Forcing.potentialPath_eq_periodic {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : EulerCylinderSmoothOrbit.pointField P (G.potentialPath I) ⋯ t = EulerPacketPeriodicPotential.field P (fun (x : EulerSmoothLimit.Space) => (D.normal.field t) x) (EulerCylinderSmoothOrbit.pointField P (G.fullVelocityPath I) ⋯ t)

This potential is exactly the manuscript's normalized angular integral of −m×A/|m|².

theorem EulerTransversePacketProvider.Forcing.corrector_formula {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.corrector I (↑t, x, θ) = EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P (G.potentialPath I) ⋯ t) (x, ↑θ) ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL (D.FInv.field t) x)

The stored corrector is the literal slow curl with the actual inverse deformation.