The actual smooth representative retains the proved compact spatial support of its L² class.

theorem EulerCylinderSmoothOrbit.representative_zero_outside (period : ℝ) [Fact (0 < period)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsClosed S) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (hs : u ∈ EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS) (x : EulerLiftedGradientSpace.LiftDomain period) (hx : x.1 ∉ S) : representative period u hu x = 0

Vanishing outside a closed support region passes from the actual L² class to its smooth representative.

theorem EulerCylinderSmoothOrbit.representative_tsupport_subset (period : ℝ) [Fact (0 < period)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsClosed S) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (hs : u ∈ EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS) : tsupport (representative period u hu) ⊆ EulerLpCylinderTranslation.spatialSet period S

The actual topological support is contained in the same closed spatial support.

theorem EulerCylinderSmoothOrbit.representative_hasCompactSupport (period : ℝ) [Fact (0 < period)] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (hs : u ∈ EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS) : HasCompactSupport (representative period u hu)

Compact spatial support remains compact after adjoining the periodic angle.