The exact corrected packet has the same primary shear, with the literal finite-tail and correction derivatives as its only errors.
noncomputable def
EulerPacketTerminalDatum.initializedExactPhysicalVelocity
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk))
(t : ↑(Set.Icc 0 D.T))
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
:
Initialized exact physical velocity as an element of Space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedExactPhysicalVelocity_eq
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk))
(t : ↑(Set.Icc 0 D.T))
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
:
initializedExactPhysicalVelocity M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk Q t Y x = initializedVelocity M D τ hτ hτT B δ hδ ξ hs α N k⁻¹ (↑t, Y x, k * inner ℝ D.m₀ (Y x)) + k⁻¹ • ((D.F.field t) (Y x))
(EulerAllOrderDriftCorrection.Budget.pointField period Q t
(EulerGraphPressurePotential.cylinderGraph period k D.m₀ (Y x)))
The approximation is exactly the finite physical velocity after undoing its true normalized coordinate transformation.
theorem
EulerPacketTerminalDatum.initializedExactPhysicalVelocity_fderiv
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk))
(t : ↑(Set.Icc 0 D.T))
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
(hY : DifferentiableAt ℝ Y x)
:
fderiv ℝ (initializedExactPhysicalVelocity M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk Q t Y) x = fderiv ℝ
(fun (y : EulerSmoothLimit.Space) =>
initializedVelocity M D τ hτ hτT B δ hδ ξ hs α N k⁻¹ (↑t, Y y, k * inner ℝ D.m₀ (Y y)))
x + fderiv ℝ
(fun (y : EulerSmoothLimit.Space) =>
k⁻¹ • ((D.F.field t) (Y y))
(EulerAllOrderDriftCorrection.Budget.pointField period Q t
(EulerGraphPressurePotential.cylinderGraph period k D.m₀ (Y y))))
x
theorem
EulerPacketTerminalDatum.initializedExactPhysicalVelocity_gradient_error
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk))
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(t : ↑(Set.Icc 0 D.T))
(X Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hX : HasFDerivAt X ((D.F.field t) 0) 0)
(hY : DifferentiableAt ℝ Y (X 0))
(hleft : ∀ (y : EulerSmoothLimit.Space), Y (X y) = y)
:
‖fderiv ℝ (initializedExactPhysicalVelocity M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk Q t Y) (X 0) - (α / δ) • ((InnerProductSpace.rankOne ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) 0))
((D.normal.field t) 0)‖ ≤ initializedRemainderDerivativeCost L.R S.H0 / k * ‖(D.FInv.field t) 0‖ + ‖fderiv ℝ
(fun (y : EulerSmoothLimit.Space) =>
k⁻¹ • ((D.F.field t) (Y y))
(EulerAllOrderDriftCorrection.Budget.pointField period Q t
(EulerGraphPressurePotential.cylinderGraph period k D.m₀ (Y y))))
(X 0)‖