Spatial support and zero angular mean of the actual affine-terminal cylinder inverse. Both properties are inherited from its genuine L² terminal datum through the explicit forced reduction.

theorem EulerCylinderDirichlet.Coefficients.frame_supported (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hu : u ∈ EulerLpCylinderPaths.Supported P U S hS) (t : ↑(Set.Icc 0 T)) : ((frame P D) t) u ∈ EulerLpCylinderPaths.Supported P E S hS

theorem EulerCylinderDirichlet.Coefficients.frameDerivative_supported (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hu : u ∈ EulerLpCylinderPaths.Supported P U S hS) (t : ↑(Set.Icc 0 T)) : ((frameDerivative P D) t) u ∈ EulerLpCylinderPaths.Supported P E S hS

theorem EulerCylinderDirichlet.Coefficients.endpointForcing_supported (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : Y ∈ EulerLpCylinderPaths.Supported P U S hS) (t : ↑(Set.Icc 0 T)) : ((endpointForcing P D) Y) t ∈ EulerLpCylinderPaths.Supported P E S hS

theorem EulerCylinderDirichlet.Coefficients.endpointCoordinate_supported (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : Y ∈ EulerLpCylinderPaths.Supported P U S hS) (t : ↑(Set.Icc 0 T)) : ((endpointCoordinate P D) Y) t ∈ EulerLpCylinderPaths.Supported P U S hS

theorem EulerCylinderDirichlet.Coefficients.endpointAcceleration_supported (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : Y ∈ EulerLpCylinderPaths.Supported P U S hS) (t : ↑(Set.Icc 0 T)) : ((endpointAcceleration P D) Y) t ∈ EulerLpCylinderPaths.Supported P U S hS

theorem EulerCylinderDirichlet.Coefficients.endpointVelocity_supported (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : Y ∈ EulerLpCylinderPaths.Supported P U S hS) (t : ↑(Set.Icc 0 T)) : ((endpointVelocity P D) Y) t ∈ EulerLpCylinderPaths.Supported P E S hS

theorem EulerCylinderDirichlet.Coefficients.endpointDerivative_supported (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : Y ∈ EulerLpCylinderPaths.Supported P U S hS) (t : ↑(Set.Icc 0 T)) : ((endpointDerivative P D) Y) t ∈ EulerLpCylinderPaths.Supported P E S hS

theorem EulerCylinderDirichlet.Coefficients.endpointForcing_mean_zero (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : (EulerCylinderAngleAverage.average P) Y = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) (((endpointForcing P D) Y) t) = 0

theorem EulerCylinderDirichlet.Coefficients.endpointCoordinate_mean_zero (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : (EulerCylinderAngleAverage.average P) Y = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) (((endpointCoordinate P D) Y) t) = 0

theorem EulerCylinderDirichlet.Coefficients.endpointAcceleration_mean_zero (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : (EulerCylinderAngleAverage.average P) Y = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) (((endpointAcceleration P D) Y) t) = 0

theorem EulerCylinderDirichlet.Coefficients.endpointVelocity_mean_zero (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : (EulerCylinderAngleAverage.average P) Y = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) (((endpointVelocity P D) Y) t) = 0

theorem EulerCylinderDirichlet.Coefficients.endpointDerivative_mean_zero (P : ℝ) [Fact (0 < P)] {T : ℝ} {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (hY : (EulerCylinderAngleAverage.average P) Y = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) (((endpointDerivative P D) Y) t) = 0