Canonical raw fields for the actual terminal-history/forward primary solution, with genuine time derivative, support, mean and tangent constraints.

Odd compact terminal data propagate through the genuine history and forward primary solve.

theorem EulerTransversePacketPrimary.forwardInitial_reflection_neg {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) (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) : (EulerCylinderFieldReflection.reflection P) ↑(forwardInitial τ hτ hτT B Y).value = -↑(forwardInitial τ hτ hτT B Y).value

theorem EulerTransversePacketPrimary.pastVelocity_reflection_neg {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) (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 τ)) : (EulerCylinderFieldReflection.reflection P) ((pastVelocity τ hτ hτT B Y) t) = -(pastVelocity τ hτ hτT B Y) t

theorem EulerTransversePacketPrimary.pastDerivative_reflection_neg {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) (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 τ)) : (EulerCylinderFieldReflection.reflection P) ((pastDerivative τ hτ hτT B Y) t) = -(pastDerivative τ hτ hτT B Y) t

theorem EulerTransversePacketPrimary.futureVelocity_reflection_neg {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 - τ))) : (EulerCylinderFieldReflection.reflection P) ((futureVelocity τ hτ hτT B Y) t) = -(futureVelocity τ hτ hτT B Y) t

theorem EulerTransversePacketPrimary.futureDerivative_reflection_neg {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 - τ))) : (EulerCylinderFieldReflection.reflection P) ((futureDerivative τ hτ hτT B Y) t) = -(futureDerivative τ hτ hτT B Y) t

theorem EulerTransversePacketPrimary.velocityPath_reflection_neg {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)) : (EulerCylinderFieldReflection.reflection P) ((velocityPath τ hτ hτT B Y) t) = -(velocityPath τ hτ hτT B Y) t

theorem EulerTransversePacketPrimary.derivativePath_reflection_neg {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)) : (EulerCylinderFieldReflection.reflection P) ((derivativePath τ hτ hτT B Y) t) = -(derivativePath τ hτ hτT B Y) t

noncomputable def EulerTransversePacketPrimary.vector {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

Vector, defined pointwise by pointField P (velocityPath τ hτ hτT B Y) (velocityPath_orbit τ hτ hτT B Y) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

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

noncomputable def EulerTransversePacketPrimary.vectorDerivative {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

Vector derivative, defined pointwise by pointField P (derivativePath τ hτ hτT B Y) (derivativePath_orbit τ hτ hτT B Y) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

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

noncomputable def EulerTransversePacketPrimary.scalar {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.ScalarField

Scalar, defined pointwise by scalarPointField P (pressurePath τ hτ hτT B Y) (pressurePath_orbit τ hτ hτT B Y) (D.clamp z.1) (z.2.1,(z.2.2 : AddCircle P)).

Equations

• EulerTransversePacketPrimary.scalar τ hτ hτT B Y z = EulerCylinderScalarPrimitive.scalarPointField P (EulerTransversePacketPrimary.pressurePath τ hτ hτT B Y) ⋯ (D.clamp z.1) (z.2.1, ↑z.2.2)

noncomputable def EulerTransversePacketPrimary.vectorField {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 (vector τ hτ hτT B Y)

Vector field, bundling path, orbit, raw_eq.

Equations

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

noncomputable def EulerTransversePacketPrimary.vectorDerivativeField {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 (vectorDerivative τ hτ hτT B Y)

Vector derivative field, bundling path, orbit, raw_eq.

Equations

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

theorem EulerTransversePacketPrimary.vectorField_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 ⋯ (vectorField τ hτ hτT B Y) (vectorDerivativeField τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.vector_hasDerivWithinAt {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) (θ : ℝ) : HasDerivWithinAt (fun (s : ℝ) => vector τ hτ hτT B Y (s, x, θ)) (vectorDerivative τ hτ hτT B Y (↑t, x, θ)) (Set.Icc 0 D.T) ↑t

theorem EulerTransversePacketPrimary.scalar_eq_pointField {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) (θ : ℝ) : scalar τ hτ hτT B Y (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P (pressurePath τ hτ hτT B Y) ⋯ t (x, ↑θ)

noncomputable def EulerTransversePacketPrimary.scalarGradientField {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 (EulerPacketCylinderField.pressureGradient (scalar τ hτ hτT B Y))

Scalar gradient field, constructed using EulerPacketCylinderField.scalarGradientField.

Equations

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

theorem EulerTransversePacketPrimary.scalar_smooth {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 : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => scalar τ hτ hτT B Y (t, y)

theorem EulerTransversePacketPrimary.vector_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) (θ : ℝ) : vector τ hτ hτT B Y (t, x, θ) = 0

theorem EulerTransversePacketPrimary.vectorDerivative_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) (θ : ℝ) : vectorDerivative τ hτ hτT B Y (t, x, θ) = 0

theorem EulerTransversePacketPrimary.vector_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 : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, vector τ hτ hτT B Y (t, x, θ) = 0

theorem EulerTransversePacketPrimary.vector_periodic {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) : Function.Periodic (fun (θ : ℝ) => vector τ hτ hτT B Y (t, x, θ)) P

theorem EulerTransversePacketPrimary.scalar_periodic {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) : Function.Periodic (fun (θ : ℝ) => scalar τ hτ hτT B Y (t, x, θ)) P

theorem EulerTransversePacketPrimary.vector_tangent {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) (θ : ℝ) : inner ℝ (D.normalField (↑t, x, θ)) (vector τ hτ hτT B Y (↑t, x, θ)) = 0

theorem EulerTransversePacketPrimary.vector_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) (θ : ℝ) : vector τ hτ hτT B Y (↑t, -x, -θ) = -vector τ hτ hτT B Y (↑t, x, θ)

theorem EulerTransversePacketPrimary.vectorDerivative_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) (θ : ℝ) : vectorDerivative τ hτ hτT B Y (↑t, -x, -θ) = -vectorDerivative τ hτ hτT B Y (↑t, x, θ)