The same forward correction used by the actual child has the literal compact initial support when the mean boundary parameter is zero.
theorem
EulerParentPacketFrames.ParticleInverse.normalized_initial
{A : Parent}
(I : ParticleInverse A)
(x : EulerSmoothLimit.Space)
:
theorem
EulerParentPacketFrames.Parent.normalizedPacketVelocity_forwardInitialized
(A : Parent)
(H : LowBounds A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(α : ℝ)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.forwardInitializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport)
⋯ δ hδ ξ hs α ⋯ N hN k hk))
(I : ParticleInverse A)
(t : ↑(Set.Icc 0 A.T))
:
A.normalizedPacketVelocity m hm J support hSupport Q
(EulerPacketTerminalDatum.forwardInitializedApproximationResidual (A.meanData H)
(A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs α ⋯ N hN k hk)
k I t = EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity (A.meanData H)
(A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs α ⋯ N hN k hk Q t (I.normalized t)
theorem
EulerParentPacketFrames.Parent.normalizedPacketPressure_forwardInitialized
(A : Parent)
(H : LowBounds A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(α : ℝ)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.forwardInitializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport)
⋯ δ hδ ξ hs α ⋯ N hN k hk))
(I : ParticleInverse A)
(t : ↑(Set.Icc 0 A.T))
:
A.normalizedPacketPressure m hm J support hSupport Q
(EulerPacketTerminalDatum.forwardInitializedApproximationResidual (A.meanData H)
(A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs α ⋯ N hN k hk)
k I t = EulerPacketTerminalDatum.forwardInitializedExactPhysicalPressure (A.meanData H)
(A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs α ⋯ N hN k hk Q t (I.normalized t)
theorem
EulerParentPacketFrames.Parent.exactForwardPacket_initial_increment_support
(A : Parent)
(H : LowBounds A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(α : ℝ)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.forwardInitializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport)
⋯ δ hδ ξ hs α ⋯ N hN k hk))
(I : ParticleInverse A)
(hL : H.L = 0)
(hS : support ⊆ Metric.closedBall 0 (1 / 2))
(u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
:
(tsupport fun (x : EulerSmoothLimit.Space) =>
A.exactPacketVelocity m hm J support hSupport Q
(EulerPacketTerminalDatum.forwardInitializedApproximationResidual (A.meanData H)
(A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs α ⋯ N hN k hk)
k I.field u (0, x) - u (0, x)) ⊆
Metric.closedBall 0 (A.ell / 2)
theorem
EulerParentPacketFrames.Parent.exactForwardPacket_initial_gradient_exterior
(A : Parent)
(H : LowBounds A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(α : ℝ)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.forwardInitializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport)
⋯ δ hδ ξ hs α ⋯ N hN k hk))
(I : ParticleInverse A)
(hL : H.L = 0)
(hS : support ⊆ Metric.closedBall 0 (1 / 2))
(u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
(hx : A.ell ≤ ‖x‖)
:
fderiv ℝ
(fun (y : EulerSmoothLimit.Space) =>
A.exactPacketVelocity m hm J support hSupport Q
(EulerPacketTerminalDatum.forwardInitializedApproximationResidual (A.meanData H)
(A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs α ⋯ N hN k hk)
k I.field u (0, y))
x = fderiv ℝ (fun (y : EulerSmoothLimit.Space) => u (0, y)) x