The actual pressure inverse in unshifted Gevrey-weighted fixed Sobolev blocks.
theorem
EulerWeightedPressure.unshifted_weighted_inverse
(ρ Rc M : ℝ)
(hρ : 0 < ρ)
(hRc : 0 ≤ Rc)
(hM : 1 ≤ M)
(hsmall : 4 * M * (ρ * Rc) ≤ 1)
(N : ℕ)
(A F Z : ℕ → ℝ)
(_hF : ∀ (n : ℕ), 0 ≤ F n)
(hZ : ∀ (n : ℕ), 0 ≤ Z n)
(hA : ∀ (l : ℕ), 1 ≤ l → l ≤ N → A l ≤ Rc ^ l * ↑l.factorial ^ 2)
(hrec : ∀ n ≤ N, Z n ≤ M * (F n + ∑ l ∈ Finset.range n, ↑(n.choose (l + 1)) * A (l + 1) * Z (n - (l + 1))))
:
∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * Z n ≤ 2 * M * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * F n
Positive-order coefficient terms are absorbed in the unshifted Gevrey sum with a constant independent of the cutoff.
theorem
EulerH6Pressure.pressure_unshifted_Hq_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)
(κ : ℝ)
(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 + q ≤ s)
(hq : q ≤ s)
(ρ Rc M : ℝ)
(hρ : 0 < ρ)
(hRc : 0 ≤ Rc)
(hM : 1 ≤ M)
(hbase : (CoefficientJet.restrict K q hq).pressureConstant c ≤ M)
(hsmall : 4 * M * (ρ * Rc) ≤ 1)
(hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → coefficientBlock period K q l ≤ Rc ^ l * ↑l.factorial ^ 2)
:
∑ n ∈ Finset.range (N + 1),
EulerPacketWeights.weight ρ n * blockNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) q n ≤ 2 * M * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * blockNorm period J q n