The direct-forward physical output costs obey the same fixed polynomial envelope, with no bound on extrema of the growth profile.

The actual finite and exact packets have the source shear at every physical point. The slow primary derivative and finite tail contribute only a fixed source constant divided by the frequency.

noncomputable def EulerPacketTerminalDatum.forwardInitializedGlobalShearCost (R H0 C : ℝ) : ℝ

Forward initialized global shear cost as an element of ℝ.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketTerminalDatum.forwardInitializedPrimary_global_bound (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) (α : ℝ) (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) : ((EulerPacketForwardPrimary.forcing D).vectorField (initialData D δ hδ (α • ξ) hs)).WordBound 6 (4 * L.R) (EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 1) 0

theorem EulerPacketTerminalDatum.forwardInitializedVelocity_global_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 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (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) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : HasFDerivAt Y ((D.FInv.field t) (Y x)) x) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => forwardInitializedVelocity M D δ hδ ξ hs α N k⁻¹ (↑t, Y y, k * inner ℝ D.m₀ (Y y))) x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) (Y x))) ((D.normal.field t) (Y x))‖ ≤ forwardInitializedGlobalShearCost L.R S.H0 NB.C / k

theorem EulerPacketTerminalDatum.forwardInitializedExactPhysicalVelocity_global_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 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (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) (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)) (hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100)) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : HasFDerivAt Y ((D.FInv.field t) (Y x)) x) : ‖fderiv ℝ (forwardInitializedExactPhysicalVelocity M D hTime δ hδ ξ hs α Cagree N hN k hk Q t Y) x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) (Y x))) ((D.normal.field t) (Y x))‖ ≤ forwardInitializedGlobalShearCost L.R S.H0 NB.C / k + ‖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 EulerPacketInitializedOutputCost.forward_output_costs {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (BC : EulerPacketCylinderField.CoefficientBudget C) (δ : ℝ) (ξ : U) (W H0 : ℝ) (hδ : 0 < δ) (H : EulerPacketForwardRadius.RadiusPrimitives L LM NB BC δ ξ W) (hH0 : 0 ≤ H0) (hHW : H0 ≤ W) : have R := EulerPacketTerminalDatum.forwardInitializedRadius LM L NB BC δ ξ; have Kc := L.correctionCoefficients NB EulerPacketTerminalDatum.period; have ρ := EulerPacketCorrectionScalar.initialRadius R Kc.M Kc.Rc / 4; have Z := EulerPacketInitializedCost.envelope W; EulerPacketInitializedCost.weightSize W ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerAllOrderDriftCorrection.physicalInputRadius (4 * R) (4 * R) ρ ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerAllOrderDriftCorrection.liftedInputConstant EulerPacketTerminalDatum.period * (EulerPacketCorrectionConstants.velocity R H0 BC.multiplierCost + EulerPacketCorrectionConstants.normal R H0 BC.multiplierCost) ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ 2 * EulerAllOrderDriftCorrection.liftedInputConstant EulerPacketTerminalDatum.period * EulerPacketInitializedCost.weightSize W ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ 2 * EulerAllOrderDriftCorrection.liftedInputConstant EulerPacketTerminalDatum.period * (6 * NB.blockAmplitude * (EulerPacketCylinderField.fixedVelocityGradeCost R H0 1 + EulerPacketCylinderField.fixedVelocityGradeCost R H0 2 + 1) + EulerPacketInitializedCost.weightSize W) ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerAllOrderDriftCorrection.weightedPhysicalGradientCost D EulerPacketTerminalDatum.period L.Rc L.C₀ ρ (EulerPacketInitializedCost.weightSize W) ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerPacketTerminalDatum.forwardInitializedGlobalShearCost R H0 NB.C ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerPacketTerminalDatum.forwardInitializedPressureHessianCost NB R H0 L.Rc L.C₀ ≤ EulerPacketPhysicalCost.extraEnvelope Z