The actual zero-history primary is the compact angular profile times the genuine homogeneous physical propagator. Its scalar pressure has the literal normal residual as its angular derivative.

theorem EulerPacketForwardFactorization.scalar_angle {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivAt (fun (s : ℝ) => EulerPacketForwardPrimary.scalar D Y (↑t, x, s)) (-(2 * inner ℝ ((D.normal.field t) x) (((D.M.field t) x) (EulerPacketForwardPrimary.vector D Y (↑t, x, θ)))) / ‖(D.normal.field t) x‖ ^ 2) θ

theorem EulerPacketForwardFactorization.vector_homogeneous_time {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Y : EulerTransversePacketProvider.InitialData P D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivWithinAt (fun (s : ℝ) => EulerPacketForwardPrimary.vector D Y (s, x, θ)) (((EulerPacketPrimaryFactorization.physicalGenerator D x) t) (EulerPacketForwardPrimary.vector D Y (↑t, x, θ))) (Set.Icc 0 D.T) ↑t

noncomputable def EulerPacketForwardFactorization.uncutVelocity {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Uncut velocity, given by physical D ⟨0,le_rfl,D.T_pos.le⟩ x ξ t.

Equations

• EulerPacketForwardFactorization.uncutVelocity D ξ t x = EulerPacketSourcePropagator.physical D ⟨0, ⋯⟩ x ξ t

noncomputable def EulerPacketForwardFactorization.canonicalVelocity {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (t : ℝ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Canonical velocity, given by innerCutoff x • uncutVelocity D ξ t x.

Equations

• EulerPacketForwardFactorization.canonicalVelocity D ξ t x = EulerSpatialCutoffs.innerCutoff x • EulerPacketForwardFactorization.uncutVelocity D ξ t x

theorem EulerPacketForwardFactorization.uncutVelocity_initial {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (x : EulerSmoothLimit.Space) : uncutVelocity D ξ 0 x = ((D.frame.field ⟨0, ⋯⟩) x) ξ

theorem EulerPacketForwardFactorization.uncutVelocity_equation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => uncutVelocity D ξ s x) (((EulerPacketPrimaryFactorization.physicalGenerator D x) t) (uncutVelocity D ξ (↑t) x)) (Set.Icc 0 D.T) ↑t

theorem EulerPacketForwardFactorization.uncutVelocity_tangent {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : inner ℝ ((D.normal.field t) x) (uncutVelocity D ξ (↑t) x) = 0

theorem EulerPacketForwardFactorization.vector_initial {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketForwardPrimary.vector D (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) (0, x, θ) = (EulerSpatialCutoffs.innerCutoff x * EulerPeriodicProfile.profile δ θ) • ((D.frame.field ⟨0, ⋯⟩) x) ξ

theorem EulerPacketForwardFactorization.vector_factorization {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketForwardPrimary.vector D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, θ) = (a * EulerPeriodicProfile.profile δ θ) • canonicalVelocity D ξ (↑t) x

theorem EulerPacketForwardFactorization.uncutVelocity_ne_zero {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (hξ : ξ ≠ 0) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : uncutVelocity D ξ (↑t) x ≠ 0