Removing the bounded time profile and performing the one final coarse factorial split.

theorem EulerPacketCylinderField.Field.WordBound.remove_profile {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hG : (G.normalized hT g hg).WordBound q R A d) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (t : ↑(Set.Icc 0 T)), g t ≤ C) : G.WordBound q R (C * A) d

theorem EulerPacketCylinderField.Field.WordBound.coarse_grade {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (hR : 1 ≤ R) (hA : 0 ≤ A) (N p : ℕ) (hN : 1 ≤ N) (hp : p ≤ 2 * N + 2) (hd : d ≤ 110 * (p + 1)) : G.WordBound q (4 * R) (A * EulerPacketCoarseMajorant.gradeBase R N ^ (p + 1)) 0

theorem EulerPacketTimeProfile.Scales.mean_le_coarse {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) (t : K) : (S.mean p) t ≤ S.H0 ^ (2 * p)

theorem EulerPacketTimeProfile.Scales.high_le_coarse {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) (hp : 1 ≤ p) (t : K) : (S.high p) t ≤ S.H0 ^ (2 * p)

theorem EulerPacketCylinderField.ProfileBudget.high_unnormalized {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (B : ProfileBudget G S R p) (hp : 1 ≤ p) : G.high.WordBound 6 R (S.H0 ^ (2 * p)) (EulerPacketShiftArithmetic.highShift p)

theorem EulerPacketCylinderField.ProfileBudget.highDerivative_unnormalized {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (B : ProfileBudget G S R p) (hp : 1 ≤ p) : G.highDerivative.WordBound 6 R (S.H0 ^ (2 * p)) (EulerPacketShiftArithmetic.highShift p)

theorem EulerPacketCylinderField.ProfileBudget.mean_unnormalized {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (B : ProfileBudget G S R p) : G.mean.WordBound 6 R (S.H0 ^ (2 * p)) (EulerPacketShiftArithmetic.meanShift p)

theorem EulerPacketCylinderField.ProfileBudget.meanDerivative_unnormalized {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (B : ProfileBudget G S R p) : G.meanDerivative.WordBound 6 R (S.H0 ^ (2 * p)) (EulerPacketShiftArithmetic.meanShift p)

theorem EulerPacketCylinderField.ProfileBudget.corrector_unnormalized {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (B : ProfileBudget G S R p) (hp : 1 ≤ p) : G.corrector.WordBound 6 R (S.H0 ^ (2 * p)) (EulerPacketShiftArithmetic.highShift p)

theorem EulerPacketCylinderField.ProfileBudget.correctorDerivative_unnormalized {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (B : ProfileBudget G S R p) (hp : 1 ≤ p) : G.correctorDerivative.WordBound 6 R (S.H0 ^ (2 * p)) (EulerPacketShiftArithmetic.highShift p)

theorem EulerPacketCylinderField.ProfileBudget.pressure_unnormalized {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (B : ProfileBudget G S R p) (hp : 1 ≤ p) : G.pressure.WordBound 6 R (S.H0 ^ (2 * p)) (EulerPacketShiftArithmetic.highShift p)