The actual base-order pressure commutator needs only one fewer pressure derivative.

noncomputable def EulerBasePressureCommutator.baseCoefficientSum (period : ℝ) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) : ℝ

Sum of the strictly positive coefficient derivative bounds at the fixed base index six.

Equations

• EulerBasePressureCommutator.baseCoefficientSum period K = ∑ l ∈ Finset.range 6, EulerJetProductBounds.boundLevel period K (l + 1)

theorem EulerBasePressureCommutator.baseCoefficientSum_nonneg (period : ℝ) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) : 0 ≤ baseCoefficientSum period K

theorem EulerBasePressureCommutator.pressure_level_le_five (period : ℝ) [Fact (0 < period)] {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 6 p) {j : ℕ} (hj : j ≤ 5) : EulerJetProductBounds.levelNorm period J j ≤ EulerH6Pressure.sobolevSize period 5 p

Every pressure derivative of order at most five is controlled by its genuine H⁵ norm.

theorem EulerBasePressureCommutator.base_order_bound (period : ℝ) [Fact (0 < period)] {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 6 p) (r : ℕ) (hr : r ≤ 6) : EulerH6Pressure.commutatorBlock K J 0 r ≤ 64 * baseCoefficientSum period K * EulerH6Pressure.sobolevSize period 5 p

At each base derivative order, the actual coefficient commutator uses only H⁵ pressure.

theorem EulerBasePressureCommutator.base_sum_bound (period : ℝ) [Fact (0 < period)] {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 6 p) : ∑ r ∈ Finset.range 7, EulerH6Pressure.commutatorBlock K J 0 r ≤ 448 * baseCoefficientSum period K * EulerH6Pressure.sobolevSize period 5 p

Summing all base orders through six leaves a fixed constant and only H⁵ pressure.

noncomputable def EulerBasePressureCommutator.basePressureBlock (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s p) (n : ℕ) (hn : n + 6 ≤ s) : ℝ

The actual base pressure commutators after an external derivative word.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerBasePressureCommutator.basePressureBlock_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s p) (n : ℕ) (hn : n + 6 ≤ s) : basePressureBlock period K J n hn ≤ 448 * baseCoefficientSum period K * EulerH6Pressure.blockNorm period J 5 n

At every external order, the base commutator loses no external derivative.

theorem EulerBasePressureCommutator.basePressure_weighted_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s p) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) : ∑ n : Fin (N + 1), EulerPacketWeights.weight ρ ↑n * basePressureBlock period K J ↑n ⋯ ≤ 448 * baseCoefficientSum period K * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period J 5 n

The complete finite weighted base pressure commutator is controlled by the unshifted H⁵ pressure sum.