Source18 for the actual coercively constructed pressure of the nonlinear transport source.

theorem EulerH6Nonlinear.blockNorm_eq_classical (period : ℝ) [Fact (0 < period)] {s q n : ℕ} {U : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s U) (h : n + q ≤ s) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑U =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : EulerH6Pressure.blockNorm period J q n = wordSobolevNorm period q n f

Actual strong-jet Hq blocks equal the classical external-word Hq norms of any smooth representative.

theorem EulerH6Nonlinear.nonlinear_pressure_shifted_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {F : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s F) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (N : ℕ) (hN : N + 6 ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (EulerH6Pressure.CoefficientJet.restrict K 6 ⋯).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period e x)) (hbL2 : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w b) 2 (EulerLiftedGradientSpace.liftMeasure period)) (heL2 : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w e) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hsource : ↑↑F =ᵐ[EulerLiftedGradientSpace.liftMeasure period] transportField period 3 b e) : ∑ n ∈ Finset.range (N + 1), ↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * EulerH6Pressure.blockNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) 6 n ≤ (4 * M * productConstant period 3 * ∑ l ∈ Finset.range (N + 2), EulerPacketWeights.weight ρ l * wordSobolevNorm period 6 l b) * ∑ j ∈ Finset.range (N + 2), ↑j * EulerPacketWeights.weight ρ j * wordSobolevNorm period 6 j e

Source18's shifted H⁶ estimate for the genuine pressure of b·∇e. The largest velocity order is N+1 and the largest pressure order is N.