The original source budgets produce actual correction budgets for all sufficiently large frequencies. Primary estimates, coefficient estimates, radius guards and frequency guards are conclusions of the construction.
One source-dependent radius accommodates the literal terminal wave, the primary endpoint solve, all later linear solves, and every recursive grade.
theorem
EulerPacketTerminalDatum.exists_initialized_budgets
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < D.T}
{B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)}
{M : EulerMeanPacketProvider.Data}
{Rm Tc : ℝ}
{O : EulerPacketProfileRecursion.Operators}
{C : EulerPacketCylinderField.CoefficientData period Tc O}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(BC : EulerPacketCylinderField.CoefficientBudget C)
(δ : ℝ)
(ξ : U)
:
∃ (L' : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (H' : EulerTransversePacketPrimary.Budget L') (N' :
EulerTransversePacketJoin.NormalBudget D 6 L'.R) (M' : EulerMeanPacketProvider.Budget M 6 L'.R),
L'.fullProfile = L.fullProfile ∧ L'.GradeGuards N' ∧ M'.GradeGuards ∧ H'.GradeGuards N' (wordCost (Fin 4) 6 δ * ‖ξ‖) ∧ wordRadius (Fin 4) δ ≤ L'.R ∧ BC.termCost ≤ L'.R ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L'.R
The terminal amplitude and the recursive grade do not enter this radius choice. The original time profile is preserved exactly.
theorem
EulerPacketTerminalDatum.initialized_correction_budgets_eventually
(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)
(Ξ : ↑(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)
:
∃ (ρ0 : ℝ) (C : ℝ),
0 < ρ0 ∧ 0 < C ∧ ∀ᶠ (k : ℝ) in Filter.atTop, ∃ (hk : 4 ≤ k) (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k)
hn k hk)),
Q.delta = EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ Q.initialRadius = ρ0 ∧ Q.growthCoefficient = C
One source-dependent initial radius and growth constant work at all sufficiently large frequencies for the literal truncation floor(k^ϑ).