Actual external pressure commutators controlled by the shifted pressure sum below the velocity cutoff.

def EulerPressureCommutatorWeights.positivePart (A : ℕ → ℝ) (n : ℕ) : ℝ

Remove the coefficient's zeroth order, which is absent from every commutator.

Equations

• EulerPressureCommutatorWeights.positivePart A n = if n = 0 then 0 else A n

def EulerPressureCommutatorWeights.delayed (P : ℕ → ℝ) : ℕ → ℝ

Delay a pressure sequence by one order so the external radius-loss convolution has the source's exact index.

Equations

• EulerPressureCommutatorWeights.delayed P 0 = 0
• EulerPressureCommutatorWeights.delayed P n.succ = P n

theorem EulerPressureCommutatorWeights.positiveCoefficientSum_bound (ρ Rc : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hsmall : ρ * Rc ≤ 1 / 2) (N : ℕ) (A : ℕ → ℝ) (hA : ∀ (l : ℕ), 1 ≤ l → l ≤ N → A l ≤ Rc ^ l * ↑l.factorial ^ 2) : ∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * positivePart A l ≤ 2 * (ρ * Rc)

The positive coefficient sum is a geometric tail, uniformly in its cutoff.

theorem EulerPressureCommutatorWeights.delayed_weighted_sum (ρ : ℝ) (N : ℕ) (P : ℕ → ℝ) : ∑ j ∈ Finset.range (N + 1), ↑j * EulerPacketWeights.weight ρ j * delayed P j = ∑ j ∈ Finset.range N, ↑(j + 1) * EulerPacketWeights.weight ρ (j + 1) * P j

The delayed pressure sum is exactly the shifted sum strictly below the cutoff.

theorem EulerPressureCommutatorWeights.commutator_weighted_shifted (ρ Rc : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hsmall : ρ * Rc ≤ 1 / 2) (N : ℕ) (A P : ℕ → ℝ) (hA0 : ∀ (l : ℕ), 0 ≤ A l) (hP : ∀ (l : ℕ), 0 ≤ P l) (hA : ∀ (l : ℕ), 1 ≤ l → l ≤ N → A l ≤ Rc ^ l * ↑l.factorial ^ 2) : ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerJetProductBounds.commutatorConvolution A P n ≤ 2 * Rc * ∑ j ∈ Finset.range N, ↑(j + 1) * EulerPacketWeights.weight ρ (j + 1) * P j

The external commutator is controlled by the shifted lower-order pressure sum, without pressure order N.

theorem EulerH6Pressure.commutatorBlock_weighted_shifted (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {p : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (P : EulerSpatialSobolevInverse.SpatialJet period directions s p) (N : ℕ) (hN : N + q ≤ s) (ρ Rc : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hsmall : ρ * Rc ≤ 1 / 2) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → coefficientBlock period K q l ≤ Rc ^ l * ↑l.factorial ^ 2) : ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * commutatorBlock K P q n ≤ 2 * Rc * ∑ j ∈ Finset.range N, ↑(j + 1) * EulerPacketWeights.weight ρ (j + 1) * blockNorm period P q j

The actual fixed-Sobolev external coefficient commutator has a bound using only the shifted pressure below the cutoff.