Uniform profile budgets bound each literal residual grade of the finite packet.

Bounds for the actual advection products in the surviving finite packet tail.

Uniform bounds on the actual finite velocity jets, including the terminal corrector.

theorem EulerPacketCylinderField.KnownPiece.profile_le_coarse {K : Type u_1} [TopologicalSpace K] (k : KnownPiece) (S : EulerPacketTimeProfile.Scales K) (i : ℕ) (hi : 1 ≤ i) (t : K) : (k.profile S i) t ≤ S.H0 ^ (2 * i)

theorem EulerPacketCylinderField.PrefixBound.piece_unnormalized {P T : ℝ} [Fact (0 < P)] {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T p a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (B : PrefixBound F hT S R) (hR : 1 ≤ R) (k : KnownPiece) (i : ℕ) (hi : 1 ≤ i) : (F.piece k i).WordBound 6 R (S.H0 ^ (2 * i)) (EulerPacketShiftArithmetic.highShift i)

theorem EulerPacketCylinderField.PrefixBound.knownJet_bound {P T : ℝ} [Fact (0 < P)] {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T p a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (B : PrefixBound F hT S R) (O : EulerPacketProfileRecursion.Operators) (hp : 2 ≤ p) (hR : 1 ≤ R) (hc : (a 0).corrector = 0) (hb : (a 1).mean = 0) (i : ℕ) : (F.knownJet O ⋯ i).field.WordBound 6 R (3 * S.H0 ^ (2 * i)) (EulerPacketShiftArithmetic.highShift i)

The literal advection fields obey the same fixed coefficient costs before the final tail split.

theorem EulerPacketCylinderField.CoefficientBudget.slow_unnormalized_bound {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (G : SpatialJetField P T J) (H : SpatialJetField P T K) {R A B : ℝ} {d e : ℕ} (hG : G.field.WordBound 6 R A d) (hH : H.field.WordBound 6 R B e) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) : (SpatialJetField.slowAdvection C.inverse G H).WordBound 6 R (BC.slowCost * A * B) (d + e + 1)

theorem EulerPacketCylinderField.CoefficientBudget.fast_unnormalized_bound {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) {J K : EulerPacketPointJets.Domain → EulerPacketPointJets.VectorJet} (G : SpatialJetField P T J) (H : SpatialJetField P T K) {R A B : ℝ} {d e : ℕ} (hG : G.field.WordBound 6 R A d) (hH : H.field.WordBound 6 R B e) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) : (SpatialJetField.fastAdvection C.normal G H).WordBound 6 R (BC.fastCost * A * B) (d + e + 1)

theorem EulerPacketCylinderField.tail_product_amplitude (H c C : ℝ) (hH : 1 ≤ H) (hc : 0 ≤ c) (hcC : c ≤ C) (i j n : ℕ) (hij : i + j ≤ n + 1) : c * (3 * H ^ (2 * i)) * (3 * H ^ (2 * j)) ≤ 9 * C * H ^ (2 * n + 2)

theorem EulerPacketCylinderField.tail_product_shift (i j n : ℕ) (hij : i + j ≤ n + 1) : EulerPacketShiftArithmetic.highShift i + EulerPacketShiftArithmetic.highShift j + 1 ≤ 110 * (n + 1)

theorem EulerPacketCylinderField.PrefixBound.tail_slow_product_bound {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T (N + 1) a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (B : PrefixBound F hT S R) {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (hN : 1 ≤ N) (hR : 1 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (hc : (a 0).corrector = 0) (hb : (a 1).mean = 0) (i j n : ℕ) (hij : i + j = n) : (SpatialJetField.slowAdvection C.inverse (F.knownJet O ⋯ i) (F.knownJet O ⋯ j)).WordBound 6 R (9 * BC.termCost * S.H0 ^ (2 * n + 2)) (110 * (n + 1))

theorem EulerPacketCylinderField.PrefixBound.tail_fast_product_bound {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T (N + 1) a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (B : PrefixBound F hT S R) {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (hN : 1 ≤ N) (hR : 1 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (hc : (a 0).corrector = 0) (hb : (a 1).mean = 0) (i j n : ℕ) (hij : i + j = n + 1) : (SpatialJetField.fastAdvection C.normal (F.knownJet O ⋯ i) (F.knownJet O ⋯ j)).WordBound 6 R (9 * BC.termCost * S.H0 ^ (2 * n + 2)) (110 * (n + 1))

The complete nonlinear tail is bounded using its actual finite convolution.

Fixed-radius word bounds for the actual finite grade convolution.

theorem EulerPacketCylinderField.Field.wordBound_convolution {P T : ℝ} [Fact (0 < P)] (M n : ℕ) (f : ℕ → ℕ → EulerPacketProfileRecursion.VectorField) (G : (i j : ℕ) → Field P T (f i j)) (q : ℕ) (R A : ℝ) (d : ℕ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hG : ∀ i ∈ Finset.range (M + 1), ∀ j ∈ Finset.range (M + 1), i + j = n → (G i j).WordBound q R A d) : (convolution M n f G).WordBound q R (↑(M + 1) ^ 2 * A) d

theorem EulerPacketCylinderField.PrefixBound.tail_nonlinear_bound {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T (N + 1) a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (B : PrefixBound F hT S R) {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (hN : 1 ≤ N) (hR : 1 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (hc : (a 0).corrector = 0) (hb : (a 1).mean = 0) (n : ℕ) : (F.tailNonlinearField C n).WordBound 6 R (18 * ↑(N + 2) ^ 2 * BC.termCost * S.H0 ^ (2 * n + 2)) (110 * (n + 1))

The only surviving linear tail grade has the same fixed coefficient budget.

theorem EulerPacketCylinderField.CoefficientBudget.linear_and_pressure_le {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) : B.linearCost + B.multiplierCost ≤ B.termCost

theorem EulerPacketCylinderField.PrefixBound.tail_linear_bound {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T (N + 1) a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (B : PrefixBound F hT S R) {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (hTime : 0 < T) (hN : 1 ≤ N) (hR : 1 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector N ⋯) Ct) (pressure : Field P T (pressureGradient (a N).highPressure)) (hCtB : (Ct.normalized hT (S.high N) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift N)) (hpB : (pressure.normalized hT (S.high N) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift N)) (n : ℕ) : (F.tailLinearField C hTime Ct hCt pressure n).WordBound 6 R (BC.termCost * S.H0 ^ (2 * n + 2)) (110 * (n + 1))

Each surviving grade of the literal packet residual has a fixed-radius estimate.

theorem EulerPacketCylinderField.PrefixBound.tail_grade_bound {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {F : PrefixFields P T (N + 1) a} {hT : 0 ≤ T} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (B : PrefixBound F hT S R) {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (hTime : 0 < T) (hN : 1 ≤ N) (hR : 1 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector N ⋯) Ct) (pressure : Field P T (pressureGradient (a N).highPressure)) (hCtB : (Ct.normalized hT (S.high N) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift N)) (hpB : (pressure.normalized hT (S.high N) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift N)) (ha : a 0 = 0) (hb : (a 1).mean = 0) (n : ℕ) (hn : N + 1 ≤ n) : (F.tailGradeField C hTime Ct hCt pressure ha n hn).WordBound 6 R ((1 + 18 * ↑(N + 2) ^ 2) * BC.termCost * S.H0 ^ (2 * n + 2)) (110 * (n + 1))

theorem EulerPacketCylinderField.ProfileRegularity.prefixThrough_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) : PrefixBound (prefixThrough hT G) ⋯ S R

theorem EulerPacketCylinderField.ProfileRegularity.tail_grade_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 : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i) (hN : 1 ≤ N) (hR : 1 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (ha : a 0 = 0) (hb : (a 1).mean = 0) (n : ℕ) (hn : N + 1 ≤ n) : (tailGradeField hT G C ha n hn).WordBound 6 R ((1 + 18 * ↑(N + 2) ^ 2) * BC.termCost * S.H0 ^ (2 * n + 2)) (110 * (n + 1))

theorem EulerPacketCylinderField.ProfileRegularity.literal_tail_grade_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 : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (BC : CoefficientBudget C) (hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i) (hN : 1 ≤ N) (hR : 1 ≤ R) (hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ R) (ha : a 0 = 0) (hb : (a 1).mean = 0) (n : ℕ) (hn : N + 1 ≤ n) : (literalTailGradeField hT G C ha n hn).WordBound 6 R ((1 + 18 * ↑(N + 2) ^ 2) * BC.termCost * S.H0 ^ (2 * n + 2)) (110 * (n + 1))