Compact support of the actual transverse potential, corrector, and their time derivatives.

theorem EulerTransversePacketProvider.Forcing.potentialPath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (G.potentialPath I) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketProvider.Forcing.potentialTimePath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (G.potentialTimePath I) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketProvider.Forcing.correctorPath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (G.correctorPath I) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketProvider.Forcing.correctorTimePath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (G.correctorTimePath I) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketProvider.Forcing.corrector_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : G.corrector I (t, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.correctorDerivative_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : G.correctorDerivative I (t, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.corrector_compact {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t θ : ℝ) : HasCompactSupport fun (x : EulerSmoothLimit.Space) => G.corrector I (t, x, θ)

theorem EulerTransversePacketProvider.Forcing.correctorDerivative_compact {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t θ : ℝ) : HasCompactSupport fun (x : EulerSmoothLimit.Space) => G.correctorDerivative I (t, x, θ)