The scalar polynomial majorant derived from the actual nonlinear Euler correction forcing.

theorem EulerGevreyNonlinearEstimate.orderZeroSource_uniform (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C0 : EulerSpatialSobolevInverse.SmoothCoefficient period) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s C0) (C : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s (C i)) (z e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (r : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (B0 B1 A0 A2 R : ℝ) (hA2 : 0 ≤ A2) (hB0 : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ z ≤ B0) (hB1 : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N ρ ((EulerCylinderSobolevSpace.derivativeOperator period s i) z) ≤ B1) (hA0 : EulerSobolevGevreyOperators.weightedCoefficient period K0 6 N ρ ≤ A0) (hA : ∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period (K i) 6 N ρ ≤ A2) (hR : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ r ≤ R) : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ (EulerGevreyOrderZero.orderZeroSource period hs L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) z r ((EulerCylinderSobolevSpace.truncateOperator period s) e)) ≤ R + (EulerH6Nonlinear.productConstant period 3 * B1 + A0 + 2 * A2 * EulerH6Nonlinear.productConstant period 3 * B0) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ e + A2 * EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ e ^ 2

Uniform bounds on the actual background and coefficient paths give the source's residual-linear-quadratic majorant.

theorem EulerGevreyNonlinearEstimate.polynomial_assembly (S T D B P B1 A0 A2 R E Y V F H : ℝ) (hS : 0 ≤ S) (hT : 0 ≤ T) (hD : 0 ≤ D) (hE : 0 ≤ E) (hY : 0 ≤ Y) (hV : V ≤ B + E) (hF : F ≤ R + (P * B1 + A0 + 2 * A2 * P * B) * E + A2 * P * E ^ 2) (hH : H ≤ S * F + T * V * E + D * V * Y) : H ≤ S * R + (S * (P * B1 + A0 + 2 * A2 * P * B) + T * B) * E + (S * A2 * P + T) * E ^ 2 + D * (B + E) * Y

The exact scalar assembly of the three already proved nonlinear forcing estimates.

theorem EulerGevreyNonlinearEstimate.correctionForcing_polynomial (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (KG : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (KG0 : 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) (hB : 0 ≤ B) (hbase5 : (EulerH6Pressure.CoefficientJet.restrict KG 5 ⋯).pressureConstant c ≤ M) (hbase6 : (EulerH6Pressure.CoefficientJet.restrict KG 6 hs).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period KG 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (hG : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period KG r ≤ B) (hG0 : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period KG0 r ≤ B) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C0 : EulerSpatialSobolevInverse.SmoothCoefficient period) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s C0) (C : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s (C i)) (z e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (r : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (B0 B1 A0 A2 R : ℝ) (hA2 : 0 ≤ A2) (hz : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ z ≤ B0) (hdz : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N ρ ((EulerCylinderSobolevSpace.derivativeOperator period s i) z) ≤ B1) (hC0 : EulerSobolevGevreyOperators.weightedCoefficient period K0 6 N ρ ≤ A0) (hC : ∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period (K i) 6 N ρ ≤ A2) (hr : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ r ≤ R) : have f := EulerGevreyOrderZero.orderZeroSource period hs L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) z r ((EulerCylinderSobolevSpace.truncateOperator period s) e); EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (EulerGevreyCorrectionForcing.correctionForcing period hs KG KG0 N hN L hL (z + e) e f ((EulerSobolevCoefficientPressure.pressureSobolevOperator period KG κ m c hc hpos) f) (EulerGevreyPressureTransport.transportPressure period hs KG κ m c hc hpos L hL (z + e) e)) ≤ EulerGevreyCorrectionBound.sourceConstant B M * R + (EulerGevreyCorrectionBound.sourceConstant B M * (EulerH6Nonlinear.productConstant period 3 * B1 + A0 + 2 * A2 * EulerH6Nonlinear.productConstant period 3 * B0) + EulerGevreyCorrectionBound.transportConstant period B M * B0) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ e + (EulerGevreyCorrectionBound.sourceConstant B M * A2 * EulerH6Nonlinear.productConstant period 3 + EulerGevreyCorrectionBound.transportConstant period B M) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ e ^ 2 + EulerGevreyCorrectionBound.lossConstant period M * (ρ⁻¹ + Rc) * (B0 + EulerSobolevGevreyOperators.weightedNorm period 6 N ρ e) * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ e

All literal forcing terms of the Euler correction have the source's scalar nonlinear majorant. Every norm and pressure in the left side is the actual constructed Sobolev object.