The actual potential and slow curl preserve the zero angular mean required by the packet recursion.

theorem EulerCylinderCorrectorMeanZero.average_primitive (P : ℝ) [Fact (0 < P)] (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) : (EulerCylinderAngleAverage.average P) ((EulerCylinderAnglePrimitive.primitive P) u) = (EulerCylinderAnglePrimitive.primitive P) ((EulerCylinderAngleAverage.average P) u)

@[instance_reducible]

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

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

Equations

• EulerCylinderCorrectorMeanZero.instCylinderCorrectorMeanZero1 P = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCylinderCorrectorMeanZero.instCylinderCorrectorMeanZero2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderCorrectorMeanZero.instCylinderCorrectorMeanZero3 (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

• EulerCylinderCorrectorMeanZero.instCylinderCorrectorMeanZero3 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderCorrectorMeanZero.instCylinderCorrectorMeanZero4 (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

• EulerCylinderCorrectorMeanZero.instCylinderCorrectorMeanZero4 P = inferInstance

theorem EulerCylinderCorrectorMeanZero.pathAverage_primitive (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) : (EulerCylinderAngleAverage.pathAverage P) ((EulerCylinderAnglePrimitive.pathPrimitive P) p) = (EulerCylinderAnglePrimitive.pathPrimitive P) ((EulerCylinderAngleAverage.pathAverage P) p)

theorem EulerCylinderCorrectorMeanZero.derivativePath_zero (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (i : Fin 4) : EulerCylinderSmoothOrbit.derivativePath P 0 i = 0

theorem EulerCylinderCorrectorMeanZero.pathAverage_derivativePath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (i : Fin 4) : (EulerCylinderAngleAverage.pathAverage P) (EulerCylinderSmoothOrbit.derivativePath P p i) = EulerCylinderSmoothOrbit.derivativePath P ((EulerCylinderAngleAverage.pathAverage P) p) i

theorem EulerCylinderCorrectorMeanZero.pathAverage_potentialPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) : (EulerCylinderAngleAverage.pathAverage P) (EulerCylinderPotential.potentialPath P B p) = EulerCylinderPotential.potentialPath P B ((EulerCylinderAngleAverage.pathAverage P) p)

theorem EulerCylinderCorrectorMeanZero.potentialPath_mean_zero (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hz : (EulerCylinderAngleAverage.pathAverage P) p = 0) : (EulerCylinderAngleAverage.pathAverage P) (EulerCylinderPotential.potentialPath P B p) = 0

theorem EulerCylinderCorrectorMeanZero.pathAverage_slowCurl (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) : (EulerCylinderAngleAverage.pathAverage P) (EulerCylinderSlowCurl.path P G p) = EulerCylinderSlowCurl.path P G ((EulerCylinderAngleAverage.pathAverage P) p)

theorem EulerCylinderCorrectorMeanZero.slowCurl_mean_zero (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hz : (EulerCylinderAngleAverage.pathAverage P) p = 0) : (EulerCylinderAngleAverage.pathAverage P) (EulerCylinderSlowCurl.path P G p) = 0