The canonical pressure Hessian of the exact forward packet differs from the literal primary normal tensor by its proved finite tail and the Hessian of the same actual correction.
theorem
EulerPacketTerminalDatum.forwardInitializedExactPhysicalPressure_hessian_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 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree N hN k hk))
(X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x)
(hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x)
(hY : Continuous (Function.uncurry Y))
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.sourceCoefficientData period M D (EulerTransversePacketProvider.InitialData.zero period D)
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 : L.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.g)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
(hdet :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
‖fderiv ℝ (gradient (forwardInitializedExactPhysicalPressure M D hTime δ hδ ξ hs α Cagree N hN k hk Q t (Y t))) x - (EulerPacketForwardShear.pressureCoefficient D ξ α t (Y t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y t x))) ((D.normal.field t) (Y t x))‖ ≤ forwardInitializedPressureHessianCost NB L.R S.H0 L.Rc L.C₀ / k + ‖fderiv ℝ (gradient (EulerAllOrderDriftCorrection.Budget.physicalPotential D period Q k Y t)) x‖