The literal corrector of the terminal-data primary solution

The actual global velocity and its true time derivative construct Q, Q_t, C and C_t. The returned Field is for the literal raw curlCorrector used by the recursion, including at the history/forward junction.

noncomputable def EulerTransversePacketPrimary.potentialPath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Potential path, given by EulerCylinderPotential.potentialPath P D.potentialCoefficientPath (velocityPath τ hτ hτT B Y).

Equations

• EulerTransversePacketPrimary.potentialPath τ hτ hτT B Y = EulerCylinderPotential.potentialPath P D.potentialCoefficientPath (EulerTransversePacketPrimary.velocityPath τ hτ hτT B Y)

noncomputable def EulerTransversePacketPrimary.potentialTimePath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Potential time path, constructed using EulerCylinderPotential.potentialDerivative.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerTransversePacketPrimary.potentialPath_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (potentialPath τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.potentialTimePath_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (potentialTimePath τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.potentialPath_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (potentialPath τ hτ hτT B Y)) ((potentialTimePath τ hτ hτT B Y) t) (Set.Icc 0 D.T) ↑t

noncomputable def EulerTransversePacketPrimary.correctorPath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Corrector path, given by EulerCylinderSlowCurl.path P D.FInv.field (potentialPath τ hτ hτT B Y).

Equations

• EulerTransversePacketPrimary.correctorPath τ hτ hτT B Y = EulerCylinderSlowCurl.path P D.FInv.field (EulerTransversePacketPrimary.potentialPath τ hτ hτT B Y)

noncomputable def EulerTransversePacketPrimary.correctorTimePath {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Corrector time path, constructed using EulerCylinderSlowCurl.derivative.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerTransversePacketPrimary.correctorPath_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (correctorPath τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.correctorTimePath_orbit {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (correctorTimePath τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.correctorPath_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ (correctorPath τ hτ hτT B Y)) ((correctorTimePath τ hτ hτT B Y) t) (Set.Icc 0 D.T) ↑t

noncomputable def EulerTransversePacketPrimary.corrector {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : EulerPacketProfileRecursion.VectorField

Corrector, defined pointwise by pointField P (correctorPath τ hτ hτT B Y) (correctorPath_orbit τ hτ hτT B Y) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• EulerTransversePacketPrimary.corrector τ hτ hτT B Y z = EulerCylinderSmoothOrbit.pointField P (EulerTransversePacketPrimary.correctorPath τ hτ hτT B Y) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketPrimary.correctorDerivative {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : EulerPacketProfileRecursion.VectorField

Corrector derivative, defined pointwise by pointField P (correctorTimePath τ hτ hτT B Y) (correctorTimePath_orbit τ hτ hτT B Y) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerTransversePacketPrimary.velocityPath_raw_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, EulerCylinderSmoothOrbit.pointField P (velocityPath τ hτ hτT B Y) ⋯ t (x, ↑θ) = 0

theorem EulerTransversePacketPrimary.rawPotential_eq {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.rawPotential P (vector τ hτ hτT B Y) (↑t, x, θ) = EulerCylinderSmoothOrbit.pointField P (potentialPath τ hτ hτT B Y) ⋯ t (x, ↑θ)

theorem EulerTransversePacketPrimary.corrector_formula {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : corrector τ hτ hτT B Y (↑t, x, θ) = EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P (potentialPath τ hτ hτT B Y) ⋯ t) (x, ↑θ) ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL (D.FInv.field t) x)

theorem EulerTransversePacketPrimary.curlCorrector_eq {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.curlCorrector P (vector τ hτ hτT B Y) (↑t, x, θ) = corrector τ hτ hτT B Y (↑t, x, θ)

noncomputable def EulerTransversePacketPrimary.correctorField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : EulerPacketCylinderField.Field P D.T (D.curlCorrector P (vector τ hτ hτT B Y))

Corrector field, bundling path, orbit, raw_eq.

Equations

• EulerTransversePacketPrimary.correctorField τ hτ hτT B Y = { path := EulerTransversePacketPrimary.correctorPath τ hτ hτT B Y, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerTransversePacketPrimary.correctorDerivativeField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : EulerPacketCylinderField.Field P D.T (correctorDerivative τ hτ hτT B Y)

Corrector derivative field, bundling path, orbit, raw_eq.

Equations

• EulerTransversePacketPrimary.correctorDerivativeField τ hτ hτT B Y = { path := EulerTransversePacketPrimary.correctorTimePath τ hτ hτT B Y, orbit := ⋯, raw_eq := ⋯ }

theorem EulerTransversePacketPrimary.correctorField_time {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : EulerPacketCylinderField.TimeDerivative ⋯ (correctorField τ hτ hτT B Y) (correctorDerivativeField τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.potentialPath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (potentialPath τ hτ hτT B Y) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketPrimary.potentialTimePath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (potentialTimePath τ hτ hτT B Y) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketPrimary.correctorPath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (correctorPath τ hτ hτT B Y) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketPrimary.correctorTimePath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (correctorTimePath τ hτ hτT B Y) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketPrimary.potentialPath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (potentialPath τ hτ hτT B Y) = 0

theorem EulerTransversePacketPrimary.potentialTimePath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (potentialTimePath τ hτ hτT B Y) = 0

theorem EulerTransversePacketPrimary.correctorPath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (correctorPath τ hτ hτT B Y) = 0

theorem EulerTransversePacketPrimary.correctorTimePath_average_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) : (EulerCylinderAngleAverage.pathAverage P) (correctorTimePath τ hτ hτT B Y) = 0

theorem EulerTransversePacketPrimary.corrector_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : corrector τ hτ hτT B Y (t, x, θ) = 0

theorem EulerTransversePacketPrimary.correctorDerivative_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : correctorDerivative τ hτ hτT B Y (t, x, θ) = 0

theorem EulerTransversePacketPrimary.curlCorrector_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, D.curlCorrector P (vector τ hτ hτT B Y) (↑t, x, θ) = 0

theorem EulerTransversePacketPrimary.curlCorrector_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hY : (EulerCylinderFieldReflection.reflection P) ↑Y.value = -↑Y.value) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.curlCorrector P (vector τ hτ hτT B Y) (↑t, -x, -θ) = -D.curlCorrector P (vector τ hτ hτT B Y) (↑t, x, θ)

theorem EulerTransversePacketPrimary.correctorDerivative_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hY : (EulerCylinderFieldReflection.reflection P) ↑Y.value = -↑Y.value) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : correctorDerivative τ hτ hτT B Y (↑t, -x, -θ) = -correctorDerivative τ hτ hτT B Y (↑t, x, θ)