The very same canonical correction has uniform all-order weighted bounds for its field, pressure and actual time derivative.

An actual canonical all-order correction from one polynomial frequency guard. This constructor does not appeal to an eventual threshold depending on a chosen parent or on an arbitrary radius witness.

noncomputable def EulerPacketTerminalDatum.initializedUniformBudget (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 < δ) (hδ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (W : ℝ) (hW : EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB (EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.fullProfile 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 ⋯ (initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) ⋯ k hk)

Initialized uniform budget used in packet initialized uniform budget.

Equations

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

theorem EulerPacketTerminalDatum.initializedUniformBudget_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τT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (W : ℝ) (hW : EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB (EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.fullProfile 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) : (initializedUniformBudget M D hTime τ hτ hτT B δ 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.initializedUniformBudget_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τT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (W : ℝ) (hW : EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB (EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.fullProfile 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) : (initializedUniformBudget M D hTime τ hτ hτT B δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog hfrequency Ξ hΞ hF hdet).initialRadius = EulerPacketCorrectionScalar.initialRadius (initializedRadius LM L NB (EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ ξ) (L.correctionCoefficients NB period).M (L.correctionCoefficients NB period).Rc

noncomputable def EulerPacketInitializedCost.weightSize (W : ℝ) : ℝ

Weight size, given by outputEnvelope period (envelope W).

Equations

• EulerPacketInitializedCost.weightSize W = EulerPacketCorrectionOutput.outputEnvelope EulerPacketTerminalDatum.period (EulerPacketInitializedCost.envelope W)

theorem EulerPacketInitializedCost.weightSize_pos (W : ℝ) (hW : 0 ≤ W) : 0 < weightSize W

theorem EulerPacketTerminalDatum.initializedUniformBudget_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τT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (α : ℝ) (hα : 0 < α) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) {Rm : ℝ} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D) (W : ℝ) (hW : EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB (EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ ξ W) (hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.fullProfile 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 ((initializedUniformBudget M D hTime τ hτ hτT B δ 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 (initializedUniformBudget M D hTime τ hτ hτT B δ 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 ((initializedUniformBudget M D hTime τ hτ hτT B δ 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 (initializedUniformBudget M D hTime τ hτ hτT B δ 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 ((initializedUniformBudget M D hTime τ hτ hτT B δ 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 (initializedUniformBudget M D hTime τ hτ hτT B δ 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)