The actual nonlinear correction forcing with explicit constants independent of the derivative cutoff.

def EulerGevreyCorrectionBound.sourceConstant (B M : ℝ) : ℝ

The coefficient multiplying the actual order-zero forcing.

Equations

• EulerGevreyCorrectionBound.sourceConstant B M = 1 + 2 * M * (3136 * B + 1)

noncomputable def EulerGevreyCorrectionBound.transportConstant (period : ℝ) [Fact (0 < period)] (B M : ℝ) : ℝ

The coefficient for actual base transport and the lower-order nonlinear pressure commutator.

Equations

• EulerGevreyCorrectionBound.transportConstant period B M = 5461 * EulerBaseTransportL2.baseTransportConstant period + 2688 * B * (8 * M * (5460 * EulerH6Nonlinear.lowerProductConstant period 3))

noncomputable def EulerGevreyCorrectionBound.lossConstant (period : ℝ) [Fact (0 < period)] (M : ℝ) : ℝ

The coefficient for the actual external radius loss.

Equations

• EulerGevreyCorrectionBound.lossConstant period M = (4 + 32 * M) * EulerH6Nonlinear.productConstant period 3

theorem EulerGevreyCorrectionBound.sourceConstant_nonneg {B M : ℝ} (hB : 0 ≤ B) (hM : 0 ≤ M) : 0 ≤ sourceConstant B M

theorem EulerGevreyCorrectionBound.transportConstant_nonneg (period : ℝ) [Fact (0 < period)] {B M : ℝ} (hB : 0 ≤ B) (hM : 0 ≤ M) : 0 ≤ transportConstant period B M

theorem EulerGevreyCorrectionBound.lossConstant_nonneg (period : ℝ) [Fact (0 < period)] {M : ℝ} (hM : 0 ≤ M) : 0 ≤ lossConstant period M

theorem EulerGevreyCorrectionBound.correctionForcing_uniform_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (κ : ℝ) (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 + 6 ≤ s) (ρ Rc M B : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase5 : (EulerH6Pressure.CoefficientJet.restrict K 5 ⋯).pressureConstant c ≤ M) (hbase6 : (EulerH6Pressure.CoefficientJet.restrict K 6 hs).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (hB : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period K r ≤ B) (hB0 : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period K0 r ≤ B) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (EulerGevreyCorrectionForcing.correctionForcing period hs K K0 N hN L hL u v f ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) f) (EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v)) ≤ sourceConstant B M * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ f + transportConstant period B M * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v + lossConstant period M * (ρ⁻¹ + Rc) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v

The actual full forcing is bounded with constants depending only on fixed base coefficient bounds and the fixed inverse majorant.