Actual inverse-frame approximate fields have bounds independent of packet length.
Inverse-frame normalized approximation bounds are independent of truncation length.
theorem
EulerPacketCylinderField.CoefficientBudget.normalized_approximation_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 k B C₁ C₂ : ℝ}
(hG : G.WordBound 6 R (k⁻¹ * C₁ + k⁻¹ ^ 2 * C₂ + 2 * B * (k⁻¹ * B) ^ 3) 0)
(hR : 0 ≤ R)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(hk : 4 ≤ k)
(hB0 : 0 ≤ B)
(hB : B ≤ k ^ (1 / 100))
(hC₁ : 0 ≤ C₁)
(hC₂ : 0 ≤ C₂)
:
theorem
EulerPacketCylinderField.ProfileRegularity.normalizedVelocity_bound
{P T : ℝ}
[Fact (0 < P)]
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(hN : 1 ≤ N)
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
((C.inverse.multiply (velocityField hT G k⁻¹)).smul k).WordBound 6 (4 * R)
(BC.multiplierCost * (fixedVelocityGradeCost R S.H0 1 + fixedVelocityGradeCost R S.H0 2 + 1)) 0
theorem
EulerPacketCylinderField.ProfileRegularity.normalizedVelocityTimeTerm_bound
{P T : ℝ}
[Fact (0 < P)]
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(hN : 1 ≤ N)
{O : EulerPacketProfileRecursion.Operators}
{C : CoefficientData P T O}
(BC : CoefficientBudget C)
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
((C.inverse.multiply (velocityDerivativeField hT G k⁻¹)).smul k).WordBound 6 (4 * R)
(BC.multiplierCost * (fixedVelocityGradeCost R S.H0 1 + fixedVelocityGradeCost R S.H0 2 + 1)) 0
This is the inverse-frame image of W_t. The derivative of the inverse frame is a separate coefficient term in the time derivative of z_a.