Explicit polynomial dependence of the fixed-order inverse on coefficient bounds.

theorem EulerH6Pressure.coefficient_restrict_level (period : ℝ) {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (hq : q ≤ s) (hn : n ≤ q) : EulerJetProductBounds.boundLevel period (CoefficientJet.restrict K q hq) n = EulerJetProductBounds.boundLevel period K n

theorem EulerH6Pressure.coefficient_child_levels {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (dA : Fin 4 → EulerSpatialSobolevInverse.SmoothCoefficient period) (lower : (i : Fin 4) → EulerSpatialSobolevInverse.CoefficientJet period directions s (dA i)) (hd : ∀ (i : Fin 4) (x : EulerLiftedGradientSpace.LiftDomain period), (dA i).coefficient x = EulerTransportDerivatives.fieldDerivative period (directions i) A.coefficient x) (L : ℝ) (h : ∀ r ≤ s + 1, EulerJetProductBounds.boundLevel period (EulerSpatialSobolevInverse.CoefficientJet.succ dA lower hd) r ≤ L) (i : Fin 4) (r : ℕ) : r ≤ s → EulerJetProductBounds.boundLevel period (lower i) r ≤ L

Uniform coefficient level bounds pass to every immediate derivative subtree.

theorem EulerH6Pressure.productConstant_polynomial {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions q A) (L : ℝ) (hL : 0 ≤ L) (hcoeff : ∀ r ≤ q, EulerJetProductBounds.boundLevel period K r ≤ L) : K.productConstant ≤ 9 ^ q * L

The fixed-order multiplier constant has an explicit polynomial bound.

theorem EulerH6Pressure.succ_le_three_pow (q : ℕ) : q + 1 ≤ 3 ^ q

A simple bound used to keep the inverse majorant polynomial at each fixed order.

theorem EulerH6Pressure.inverse_majorant_dominates (q : ℕ) {L : ℝ} (hL : 1 ≤ L) : 9 * (9 ^ q * L) ≤ (9 * L) ^ 3 ^ q

The inverse majorant dominates nine times the fixed-order multiplier majorant.

theorem EulerH6Pressure.inverse_majorant_step {L B M : ℝ} (hL : 1 ≤ L) (hB : L ≤ B) (hM : 9 * B ≤ M) : L + 4 * (M * (1 + B * M)) ≤ M ^ 3

One stage of the explicit polynomial inverse bound.

theorem EulerH6Pressure.pressureConstant_polynomial {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions q A) (c L : ℝ) (hc : 0 < c) (hL : 1 ≤ L) (hcL : c⁻¹ ≤ L) (hcoeff : ∀ r ≤ q, EulerJetProductBounds.boundLevel period K r ≤ L) : K.pressureConstant c ≤ (9 * L) ^ 3 ^ q

Every fixed-order coercive inverse constant is bounded by an explicit polynomial in L. At the source's Sobolev index6 the exponent is729, independent of the external cutoff.

theorem EulerH6Pressure.pressure_shifted_Hq_polynomial_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) (L ρ Rc : ℝ) (hL : 1 ≤ L) (hcL : c⁻¹ ≤ L) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hbasecoeff : ∀ r ≤ q, EulerJetProductBounds.boundLevel period K r ≤ L) (hsmall : 4 * (9 * L) ^ 3 ^ q * (ρ * 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 * (9 * L) ^ 3 ^ q * ∑ n ∈ Finset.range (N + 1), ↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * blockNorm period J q n

The shifted Hq pressure estimate with an explicit polynomial coefficient constant. All assumptions concern the actual coefficient, its derivative bounds, and coercivity.