The actual zero-history correction from the same fixed polynomial frequency comparison, together with its uniform weighted output bounds.

noncomputable def EulerPacketTerminalDatum.forwardUniformBudget (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δ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (W : ℝ) (hW : EulerPacketForwardRadius.RadiusPrimitives L LM NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.g t ≤ W) (k : ℝ) (hk : 4 ≤ k) (hX : 64 ≤ EulerPacketSourceFrequency.expansion k) (hlog : 1 ≤ Real.log k) (hfrequency : EulerPacketInitializedCost.uniformConstant * W ^ EulerPacketInitializedCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k) (Ξ : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (Ξ t)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (Ξ t) x = (D.F.field t) x) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) : EulerAllOrderDriftCorrection.Budget period ⋯ (forwardInitializedCorrectionData M D hTime δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) ⋯ k hk)

Forward uniform budget used in packet forward uniform budget.

Equations

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

theorem EulerPacketTerminalDatum.forwardUniformBudget_delta (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δ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (W : ℝ) (hW : EulerPacketForwardRadius.RadiusPrimitives L LM NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.g t ≤ W) (k : ℝ) (hk : 4 ≤ k) (hX : 64 ≤ EulerPacketSourceFrequency.expansion k) (hlog : 1 ≤ Real.log k) (hfrequency : EulerPacketInitializedCost.uniformConstant * W ^ EulerPacketInitializedCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k) (Ξ : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (Ξ t)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (Ξ t) x = (D.F.field t) x) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) : (forwardUniformBudget M D hTime δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet).delta = EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k)

theorem EulerPacketTerminalDatum.forwardUniformBudget_initialRadius (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δ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (W : ℝ) (hW : EulerPacketForwardRadius.RadiusPrimitives L LM NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.g t ≤ W) (k : ℝ) (hk : 4 ≤ k) (hX : 64 ≤ EulerPacketSourceFrequency.expansion k) (hlog : 1 ≤ Real.log k) (hfrequency : EulerPacketInitializedCost.uniformConstant * W ^ EulerPacketInitializedCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k) (Ξ : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (Ξ t)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (Ξ t) x = (D.F.field t) x) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) : (forwardUniformBudget M D hTime δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet).initialRadius = EulerPacketCorrectionScalar.initialRadius (forwardInitializedRadius LM L NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ) (L.correctionCoefficients NB period).M (L.correctionCoefficients NB period).Rc

theorem EulerPacketTerminalDatum.forwardUniformBudget_weighted (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δ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (W : ℝ) (hW : EulerPacketForwardRadius.RadiusPrimitives L LM NB (EulerPacketCylinderField.forwardCoefficientBudget period M D hTime NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.g t ≤ W) (k : ℝ) (hk : 4 ≤ k) (hX : 64 ≤ EulerPacketSourceFrequency.expansion k) (hlog : 1 ≤ Real.log k) (hfrequency : EulerPacketInitializedCost.uniformConstant * W ^ EulerPacketInitializedCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k) (Ξ : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (Ξ t)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (Ξ t) x = (D.F.field t) x) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (s N : ℕ) (hN : N + 6 ≤ s) (t : ↑(Set.Icc 0 D.T)) : EulerSobolevGevreyOperators.weightedNorm period 6 N ((forwardUniformBudget M D hTime δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet).initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.fieldTower period (forwardUniformBudget M D hTime δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet)).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 N ((forwardUniformBudget M D hTime δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet).initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.pressureTower period (forwardUniformBudget M D hTime δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet)).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 N ((forwardUniformBudget M D hTime δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet).initialRadius / 4) (((EulerAllOrderDriftCorrection.Budget.timeDerivativeTower period (forwardUniformBudget M D hTime δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet)).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k)