The actual primary field on the full history-plus-forward interval. Only the history interval uses the coercive endpoint solve. The forward interval uses its true coordinate trace, and gluing preserves the actual time derivative and the mixed translation orbit.

The primary history has prescribed terminal displacement. Its actual coordinate velocity at τ is the initial value of the homogeneous forward solve. Both the physical velocity and its true derivative match at τ.

noncomputable def EulerTransversePacketPrimary.zeroForcing {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : EulerTransversePacketProvider.Forcing P D 0

Zero forcing, bundling path, path_orbit, raw_eq, mean_zero.

Equations

• EulerTransversePacketPrimary.zeroForcing D = { path := 0, path_orbit := ⋯, raw_eq := ⋯, mean_zero := ⋯ }

def EulerTransversePacketPrimary.endpointData {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (Y : EulerTransversePacketProvider.InitialData P D) : EulerTransversePacketProvider.InitialData P (D.initial τ hτ ⋯)

Endpoint data, bundling value, orbit, mean_zero.

Equations

• EulerTransversePacketPrimary.endpointData τ hτ hτT Y = { value := Y.value, orbit := ⋯, mean_zero := ⋯ }

noncomputable def EulerTransversePacketPrimary.forwardInitial {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) : EulerTransversePacketProvider.InitialData P (D.tail τ ⋯ hτT)

Forward initial, bundling value, orbit, mean_zero.

Equations

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

noncomputable def EulerTransversePacketPrimary.pastVelocity {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 τ), ↥(EulerLiftedGradientSpace.LiftL2 P))

Past velocity, given by EulerTransversePacketEndpoint.velocityPath B (endpointData τ hτ hτT Y).

Equations

• EulerTransversePacketPrimary.pastVelocity τ hτ hτT B Y = EulerTransversePacketEndpoint.velocityPath B (EulerTransversePacketPrimary.endpointData τ hτ hτT Y)

noncomputable def EulerTransversePacketPrimary.pastDerivative {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 τ), ↥(EulerLiftedGradientSpace.LiftL2 P))

Past derivative, given by EulerTransversePacketEndpoint.derivativePath B (endpointData τ hτ hτT Y).

Equations

• EulerTransversePacketPrimary.pastDerivative τ hτ hτT B Y = EulerTransversePacketEndpoint.derivativePath B (EulerTransversePacketPrimary.endpointData τ hτ hτT Y)

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

Future velocity, given by includePath P D.support D.support_measurable ((zeroForcing (D.tail τ hτ.le hτT)).velocityPath (forwardInitial τ hτ hτT B Y)).

Equations

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

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

Future derivative, given by includePath P D.support D.support_measurable ((zeroForcing (D.tail τ hτ.le hτT)).derivativePath (forwardInitial τ hτ hτT B Y)).

Equations

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

theorem EulerTransversePacketPrimary.pastVelocity_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) (pastVelocity τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.pastDerivative_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) (pastDerivative τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.futureVelocity_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) (futureVelocity τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.futureDerivative_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) (futureDerivative τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.velocity_match {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) : (pastVelocity τ hτ hτT B Y) ⟨τ, ⋯⟩ = (futureVelocity τ hτ hτT B Y) ⟨0, ⋯⟩

theorem EulerTransversePacketPrimary.past_balance_ae {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 τ)) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, ↑↑((pastDerivative τ hτ hτT B Y) t) x + (((D.initial τ hτ ⋯).M.field t) x.1) (↑↑((pastVelocity τ hτ hτT B Y) t) x) + (-(2 * inner ℝ (((D.initial τ hτ ⋯).normal.field t) x.1) ((((D.initial τ hτ ⋯).M.field t) x.1) (↑↑((pastVelocity τ hτ hτT B Y) t) x))) / ‖((D.initial τ hτ ⋯).normal.field t) x.1‖ ^ 2) • ((D.initial τ hτ ⋯).normal.field t) x.1 = 0

theorem EulerTransversePacketPrimary.future_balance_ae {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 : EulerLiftedGradientSpace.LiftDomain P) ∂EulerLiftedGradientSpace.liftMeasure P, ↑↑((futureDerivative τ hτ hτT B Y) t) x + (((D.tail τ ⋯ hτT).M.field t) x.1) (↑↑((futureVelocity τ hτ hτT B Y) t) x) + (-(2 * inner ℝ (((D.tail τ ⋯ hτT).normal.field t) x.1) ((((D.tail τ ⋯ hτT).M.field t) x.1) (↑↑((futureVelocity τ hτ hτT B Y) t) x))) / ‖((D.tail τ ⋯ hτT).normal.field t) x.1‖ ^ 2) • ((D.tail τ ⋯ hτT).normal.field t) x.1 = 0

theorem EulerTransversePacketPrimary.derivative_match {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) : (pastDerivative τ hτ hτT B Y) ⟨τ, ⋯⟩ = (futureDerivative τ hτ hτT B Y) ⟨0, ⋯⟩

theorem EulerTransversePacketPrimary.pastVelocity_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 τ)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath τ ⋯ (pastVelocity τ hτ hτT B Y)) ((pastDerivative τ hτ hτT B Y) t) (Set.Icc 0 τ) ↑t

theorem EulerTransversePacketPrimary.futureVelocity_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 - τ) ⋯ (futureVelocity τ hτ hτT B Y)) ((futureDerivative τ hτ hτT B Y) t) (Set.Icc 0 (D.T - τ)) ↑t

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

Velocity path, given by join D.T τ hτ.le hτT.le (pastVelocity τ hτ hτT B Y) (futureVelocity τ hτ hτT B Y) (velocity_match τ hτ hτT B Y).

Equations

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

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

Derivative path, given by join D.T τ hτ.le hτT.le (pastDerivative τ hτ hτT B Y) (futureDerivative τ hτ hτT B Y) (derivative_match τ hτ hτT B Y).

Equations

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

noncomputable def EulerTransversePacketPrimary.pressurePath {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), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

Pressure path, given by sourcePressure P D.M D.normal D.normalLower D.normalLower_pos D.normal_lower 0 (velocityPath τ hτ hτT B Y).

Equations

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

theorem EulerTransversePacketPrimary.velocityPath_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) (velocityPath τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.derivativePath_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) (derivativePath τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.pressurePath_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) (pressurePath τ hτ hτT B Y)

theorem EulerTransversePacketPrimary.velocityPath_left {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 τ)) : (velocityPath τ hτ hτT B Y) ⟨↑t, ⋯⟩ = (pastVelocity τ hτ hτT B Y) t

theorem EulerTransversePacketPrimary.derivativePath_left {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 τ)) : (derivativePath τ hτ hτT B Y) ⟨↑t, ⋯⟩ = (pastDerivative τ hτ hτT B Y) t

theorem EulerTransversePacketPrimary.velocityPath_right {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 τ D.T)) : (velocityPath τ hτ hτT B Y) ⟨↑t, ⋯⟩ = (futureVelocity τ hτ hτT B Y) ⟨↑t - τ, ⋯⟩

theorem EulerTransversePacketPrimary.derivativePath_right {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 τ D.T)) : (derivativePath τ hτ hτT B Y) ⟨↑t, ⋯⟩ = (futureDerivative τ hτ hτT B Y) ⟨↑t - τ, ⋯⟩

theorem EulerTransversePacketPrimary.velocityPath_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 ⋯ (velocityPath τ hτ hτT B Y)) ((derivativePath τ hτ hτT B Y) t) (Set.Icc 0 D.T) ↑t

theorem EulerTransversePacketPrimary.velocityPath_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)) : (velocityPath τ hτ hτT B Y) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketPrimary.derivativePath_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)) : (derivativePath τ hτ hτT B Y) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketPrimary.velocityPath_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)) : (EulerCylinderAngleAverage.average P) ((velocityPath τ hτ hτT B Y) t) = 0

theorem EulerTransversePacketPrimary.derivativePath_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)) : (EulerCylinderAngleAverage.average P) ((derivativePath τ hτ hτT B Y) t) = 0