Actual inverse-frame normalization preserves the exponentially small residual estimate.
theorem
EulerPacketCylinderField.CoefficientBudget.normalized_inverse_bound
{P T : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
{R A : ℝ}
{d : ℕ}
(hG : G.WordBound 6 R A d)
(hA : 0 ≤ A)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(k : ℝ)
(hk : 0 ≤ k)
:
theorem
EulerPacketCylinderField.CoefficientBudget.normalized_tail_exponential
{P T : ℝ}
[Fact (0 < P)]
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
{R B k X : ℝ}
(N : ℕ)
(hG : G.WordBound 6 R (2 * B * (k⁻¹ * B) ^ (N + 1)) 0)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(hR : 0 ≤ R)
(hk : 4 ≤ k)
(hB0 : 0 ≤ B)
(hB : B ≤ k ^ (1 / 100))
(hC : BC.multiplierCost ≤ k ^ (1 / 100))
(hX : 6 ≤ X)
(hN : X - 1 ≤ ↑N)
: