The uncut primary is the genuine homogeneous physical evolution of the actual stationary history's initial coordinate. Its all-time relation to the compactly supported packet is proved by ODE uniqueness.
theorem
EulerPacketPrimaryFactorization.historyVelocity_homogeneous
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(B : EulerTransversePacketProvider.HistoryData D)
(ξ : U)
(x : EulerSmoothLimit.Space)
(t : ↑(Set.Icc 0 D.T))
:
HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ ((B.coefficients.labelVelocity x) ξ))
(((physicalGenerator D x) t) (((B.coefficients.labelVelocity x) ξ) t)) (Set.Icc 0 D.T) ↑t
noncomputable def
EulerPacketPrimaryFactorization.uncutVelocity
{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τ ⋯))
(ξ : U)
(t : ℝ)
(x : EulerSmoothLimit.Space)
:
Uncut velocity, given by physical D ⟨0,le_rfl,D.T_pos.le⟩ x (B.coefficients.labelCoordinate x ξ ⟨0,le_rfl,hτ.le⟩) t.
Equations
- EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT B ξ t x = EulerPacketSourcePropagator.physical D ⟨0, ⋯⟩ x (((B.coefficients.labelCoordinate x) ξ) ⟨0, ⋯⟩) t
Instances For
theorem
EulerPacketPrimaryFactorization.uncutVelocity_initial
{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τ ⋯))
(ξ : U)
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketPrimaryFactorization.uncutVelocity_equation
{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τ ⋯))
(ξ : U)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
HasDerivWithinAt (fun (s : ℝ) => uncutVelocity τ hτ hτT B ξ s x)
(((physicalGenerator D x) t) (uncutVelocity τ hτ hτT B ξ (↑t) x)) (Set.Icc 0 D.T) ↑t
theorem
EulerPacketPrimaryFactorization.uncutVelocity_tangent
{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τ ⋯))
(ξ : U)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketPrimaryFactorization.uncutVelocity_history
{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τ ⋯))
(ξ : U)
(t : ↑(Set.Icc 0 τ))
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketPrimaryFactorization.canonicalVelocity_eq_cutoff_uncut
{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τ ⋯))
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
canonicalVelocity τ hτ hτT B ξ hs (↑t) x = EulerSpatialCutoffs.innerCutoff x • uncutVelocity τ hτ hτT B ξ (↑t) x
theorem
EulerPacketPrimaryFactorization.uncutVelocity_ne_zero
{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τ ⋯))
(ξ : U)
(hξ : ξ ≠ 0)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketPrimaryFactorization.vector_uncut_factorization
{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τ ⋯))
(ξ : U)
(δ : ℝ)
(hδ : 0 < δ)
(a : ℝ)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, θ) = (a * EulerSpatialCutoffs.innerCutoff x * EulerPeriodicProfile.profile δ θ) • uncutVelocity τ hτ hτT B ξ (↑t) x