The actual chosen packet states preserve common compact initial support. The forward mean contribution is localized even when its boundary coefficient is nonzero.

theorem EulerPacketTerminalDatum.forwardInitializedInitialMean_support (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hTime : M.T = D.T) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (N : ℕ) (k : ℝ) : tsupport (forwardInitializedInitialMean M D δ hδ ξ hs α N k) ⊆ Metric.closedBall 0 2

theorem EulerPacketTerminalDatum.forwardInitializedInitial_common_support (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hTime : M.T = D.T) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hS : D.support ⊆ Metric.closedBall 0 (1 / 2)) (N : ℕ) (k : ℝ) : tsupport (forwardInitializedInitialHigh M D δ hδ ξ hs α N k) ⊆ Metric.closedBall 0 2 ∧ tsupport (forwardInitializedInitialMean M D δ hδ ξ hs α N k) ⊆ Metric.closedBall 0 2

theorem EulerParentPacketFrames.support_of_difference (f g : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (R : ℝ) (hf : tsupport f ⊆ Metric.closedBall 0 R) (hd : tsupport (g - f) ⊆ Metric.closedBall 0 R) : tsupport g ⊆ Metric.closedBall 0 R

theorem EulerParentPacketFrames.GeometryForwardInput.initial_support {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (k : ℝ) : tsupport (I.high k) ⊆ Metric.closedBall 0 2 ∧ tsupport (I.mean k) ⊆ Metric.closedBall 0 2

theorem EulerParentPacketFrames.GeometryForwardChoice.initial_support {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (hS : (tsupport fun (x : EulerSmoothLimit.Space) => S.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2) : (tsupport fun (x : EulerSmoothLimit.Space) => (state I S k hk nextEll hnext hnext1 F hSym).evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2

theorem EulerParentPacketFrames.GeometryForwardChoice.initial_compact {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (hS : (tsupport fun (x : EulerSmoothLimit.Space) => S.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2) : HasCompactSupport fun (x : EulerSmoothLimit.Space) => (state I S k hk nextEll hnext hnext1 F hSym).evolution.velocity (0, x)

theorem EulerParentPacketFrames.GeometryJoinedChoice.initial_support {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : EulerPacketInitial.Input U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryJoinedChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) (hS : (tsupport fun (x : EulerSmoothLimit.Space) => S.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2) : (tsupport fun (x : EulerSmoothLimit.Space) => (state I S k hk nextEll hnext hnext1 F hSym).evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2