Actual support and angular normalization of the joined transverse provider.

theorem EulerElapsedTimePathGluing.join_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S τ : ℝ) (hτ0 : 0 ≤ τ) (hτS : τ ≤ S) (u : C(↑(Set.Icc 0 τ), E)) (v : C(↑(Set.Icc 0 (S - τ)), E)) (hm : u ⟨τ, ⋯⟩ = v ⟨0, ⋯⟩) (J : Set E) (hu : ∀ (t : ↑(Set.Icc 0 τ)), u t ∈ J) (hv : ∀ (t : ↑(Set.Icc 0 (S - τ))), v t ∈ J) (t : ↑(Set.Icc 0 S)) : (join S τ hτ0 hτS u v hm) t ∈ J

theorem EulerTransversePacketJoin.velocityPath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) : (velocityPath τ hτ hτT B G) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketJoin.derivativePath_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) : (derivativePath τ hτ hτT B G) t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketJoin.velocityPath_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) : (EulerCylinderAngleAverage.average P) ((velocityPath τ hτ hτT B G) t) = 0

theorem EulerTransversePacketJoin.vector_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : vector τ hτ hτT B G (t, x, θ) = 0

theorem EulerTransversePacketJoin.vectorDerivative_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : vectorDerivative τ hτ hτT B G (t, x, θ) = 0

theorem EulerTransversePacketJoin.vector_mean_zero {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, vector τ hτ hτT B G (t, x, θ) = 0

theorem EulerTransversePacketJoin.scalar_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : scalar τ hτ hτT B G (↑t, x, θ) = 0

theorem EulerTransversePacketJoin.scalar_normalized {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, scalar τ hτ hτT B G (↑t, x, θ) = 0

theorem EulerTransversePacketJoin.vector_periodic {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ℝ) (x : EulerSmoothLimit.Space) : Function.Periodic (fun (θ : ℝ) => vector τ hτ hτT B G (t, x, θ)) P

theorem EulerTransversePacketJoin.scalar_periodic {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (t : ℝ) (x : EulerSmoothLimit.Space) : Function.Periodic (fun (θ : ℝ) => scalar τ hτ hτT B G (t, x, θ)) P