Actual unshifted Gevrey product and lower-pressure estimates with constants independent of truncation.

theorem EulerWeightedConvolution.unshifted_product_term (ρ : ℝ) (hρ : 0 < ρ) (j l : ℕ) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : EulerPacketWeights.weight ρ (j + l) * ↑((j + l).choose l) * a * b ≤ EulerPacketWeights.weight ρ l * a * (EulerPacketWeights.weight ρ j * b)

The ordinary Gevrey-two product weight is submultiplicative after paying the binomial coefficient.

theorem EulerWeightedConvolution.unshifted_product_sum (ρ : ℝ) (hρ : 0 < ρ) (N : ℕ) (A B : ℕ → ℝ) (hA : ∀ (n : ℕ), 0 ≤ A n) (hB : ∀ (n : ℕ), 0 ≤ B n) : ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerJetProductBounds.leibnizConvolution A B n ≤ (∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * A l) * ∑ j ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ j * B j

The actual binomial product convolution is bounded in unshifted Gevrey sums with constant one.

theorem EulerH6Nonlinear.product_unshifted_weighted_bound (period : ℝ) [Fact (0 < period)] (d N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (f : EulerLiftedGradientSpace.LiftDomain period → ℝ) (g : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain d) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : (∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * wordSobolevNorm period 6 n fun (x : EulerLiftedGradientSpace.LiftDomain period) => f x • g x) ≤ (productConstant period d * ∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * wordSobolevNorm period 6 l f) * ∑ j ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ j * wordSobolevNorm period 6 j g

The actual scalar-vector product is bounded in every finite unshifted H⁶ Gevrey sum.

theorem EulerH6Nonlinear.transport_lower_weighted_bound (period : ℝ) [Fact (0 < period)] (N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (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)) (hbL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w b) 2 (EulerLiftedGradientSpace.liftMeasure period)) (heL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w e) 2 (EulerLiftedGradientSpace.liftMeasure period)) : ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * wordSobolevNorm period 5 n (transportField period 3 b e) ≤ (5460 * lowerProductConstant period 3 * ∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * wordSobolevNorm period 6 l b) * ∑ j ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ j * wordSobolevNorm period 6 j e

The actual transport source in H⁵ is bounded by H⁶ energies at the same external cutoff.

theorem EulerH6Pressure.multiply_block_weighted_bound (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) : ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * blockNorm period (EulerSpatialSobolevInverse.SpatialJet.multiply K J) q n ≤ (∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * coefficientBlock period K q l) * ∑ j ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ j * blockNorm period J q j

Actual coefficient multiplication has its unshifted weighted fixed-Sobolev bound.