The actual coercive pressure inverse in fixed Sobolev blocks, followed by external Gevrey weighting.
theorem
EulerH6Pressure.pressure_sobolevSize_bound
(period : ℝ)
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{q : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
{f : ↥(EulerLiftedGradientSpace.LiftL2 period)}
(K : EulerSpatialSobolevInverse.CoefficientJet period directions q A)
(J : EulerSpatialSobolevInverse.SpatialJet period directions q 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)
:
The already-constructed coercive inverse is bounded in the genuine fixed-order Sobolev norm.
theorem
EulerH6Pressure.pressure_block_inverse
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s q n : ℕ}
{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)
(hq : q ≤ s)
(h : n + q ≤ s)
:
blockNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) q n ≤ (CoefficientJet.restrict K q hq).pressureConstant c * (blockNorm period J q n + commutatorBlock K (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) q n)
Apply the fixed-order Sobolev inverse separately to every actual external derivative word.
theorem
EulerH6Pressure.pressure_block_recurrence
{period : ℝ}
[Fact (0 < period)]
{directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent}
{s q n : ℕ}
{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)
(hq : q ≤ s)
(h : n + q ≤ s)
(M : ℝ)
(hM : (CoefficientJet.restrict K q hq).pressureConstant c ≤ M)
:
blockNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) q n ≤ M * (blockNorm period J q n + ∑ l ∈ Finset.range n,
↑(n.choose (l + 1)) * coefficientBlock period K q (l + 1) * blockNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) q (n - (l + 1)))
The pressure recurrence has the required external-order binomial coefficients and Hq blocks.
theorem
EulerH6Pressure.pressure_shifted_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),
↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * blockNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) q n ≤ 2 * M * ∑ n ∈ Finset.range (N + 1), ↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * blockNorm period J q n
Source equation18's shifted inverse estimate in genuine fixed Hq blocks. The constant depends on q and base coefficient bounds, and is independent of the external cutoff N.