The actual primary retains its angular profile on the entire joined interval. This follows from uniqueness for its genuine homogeneous linear ODE, whose coefficients are independent of the angle.
@[instance_reducible]
Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
Cache the standard NormedSpace ℝ Space instance to shorten typeclass synthesis.
Instances For
noncomputable def
EulerPacketPrimaryFactorization.physicalGenerator
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(x : EulerSmoothLimit.Space)
:
Physical generator, bundling toFun, continuous_toFun, have, have.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketPrimaryFactorization.physicalGenerator_apply
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(x : EulerSmoothLimit.Space)
(t : ↑(Set.Icc 0 D.T))
(v : EulerSmoothLimit.Space)
:
theorem
EulerPacketPrimaryFactorization.vector_homogeneous_time
{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τ ⋯))
{P : ℝ}
[Fact (0 < P)]
(Y : EulerTransversePacketProvider.InitialData P D)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ : ℝ)
:
HasDerivWithinAt (fun (s : ℝ) => EulerTransversePacketPrimary.vector τ hτ hτT B Y (s, x, θ))
(((physicalGenerator D x) t) (EulerTransversePacketPrimary.vector τ hτ hτT B Y (↑t, x, θ))) (Set.Icc 0 D.T) ↑t
theorem
EulerPacketPrimaryFactorization.angular_proportional
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(θ φ : ℝ)
:
EulerPeriodicProfile.profile δ φ • EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) (↑t, x, θ) = EulerPeriodicProfile.profile δ θ • EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) (↑t, x, φ)
noncomputable def
EulerPacketPrimaryFactorization.envelopedVelocity
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ℝ)
(x : EulerSmoothLimit.Space)
:
The envelope is retained in this actual velocity. On the core it agrees with the unmultiplied history, and its definition is valid for every time.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketPrimaryFactorization.vector_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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(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δ ξ hs) (↑t, x, θ) = EulerPeriodicProfile.profile δ θ • envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) x
theorem
EulerPacketPrimaryFactorization.envelopedVelocity_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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 τ))
(x : EulerSmoothLimit.Space)
:
envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) x = EulerSpatialCutoffs.innerCutoff x • ((B.coefficients.labelVelocity x) ξ) t
theorem
EulerPacketPrimaryFactorization.envelopedVelocity_homogeneous_time
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
HasDerivWithinAt (fun (s : ℝ) => envelopedVelocity τ hτ hτT B δ hδ ξ hs s x)
(((physicalGenerator D x) t) (envelopedVelocity τ hτ hτT B δ hδ ξ hs (↑t) x)) (Set.Icc 0 D.T) ↑t
theorem
EulerPacketPrimaryFactorization.envelopedVelocity_independent_profile
{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τ ⋯))
(δ δ' : ℝ)
(hδ : 0 < δ)
(hδ' : 0 < δ')
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
The recovered velocity is independent of the narrow angular profile. In particular its construction does not introduce a dependence on δ into the geometric amplitude or the homogeneous propagation estimate.
noncomputable def
EulerPacketPrimaryFactorization.canonicalVelocity
{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 : ℝ)
(x : EulerSmoothLimit.Space)
:
Canonical velocity, given by envelopedVelocity τ hτ hτT B 1 zero_lt_one ξ hs t x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketPrimaryFactorization.vector_factorization_canonical
{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τ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(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δ ξ hs) (↑t, x, θ) = EulerPeriodicProfile.profile δ θ • canonicalVelocity τ hτ hτT B ξ hs (↑t) x
theorem
EulerPacketPrimaryFactorization.canonicalVelocity_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)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(t : ↑(Set.Icc 0 τ))
(x : EulerSmoothLimit.Space)
:
canonicalVelocity τ hτ hτT B ξ hs (↑t) x = EulerSpatialCutoffs.innerCutoff x • ((B.coefficients.labelVelocity x) ξ) t
theorem
EulerPacketPrimaryFactorization.canonicalVelocity_homogeneous_time
{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)
:
HasDerivWithinAt (fun (s : ℝ) => canonicalVelocity τ hτ hτT B ξ hs s x)
(((physicalGenerator D x) t) (canonicalVelocity τ hτ hτT B ξ hs (↑t) x)) (Set.Icc 0 D.T) ↑t