The actual nonlinear viscous correction closes its shrinking-radius Gevrey bootstrap from the constructed mild equation.

Separate the full background norm from the drift norm in the radius-loss term.

noncomputable def EulerDriftEnergyConstants.forcingPolynomial (period : ℝ) [Fact (0 < period)] (B M Z0 B0 B1 A0 A2 residual c Rc ρ X Y : ℝ) : ℝ

The full velocity enters the zero-order coefficient; only the drift enters the loss term.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerDriftEnergyConstants.actual_scalar_bound (period : ℝ) [Fact (0 < period)] (g0 g1 k B M Z0 B0 B1 A0 A2 c Rc ρ residual X Y b : ℝ) (hg0 : 0 ≤ g0) (hg1 : 0 ≤ g1) (hk : 0 ≤ k) (hB : 0 ≤ B) (hM : 0 ≤ M) (hZ0 : 0 ≤ Z0) (hB0 : 0 ≤ B0) (hB1 : 0 ≤ B1) (hA0 : 0 ≤ A0) (hA2 : 0 ≤ A2) (hc : 0 < c) (hRc : 0 ≤ Rc) (hρ : 0 < ρ) (hr : 0 ≤ residual) (hX : 0 ≤ X) (hY : 0 ≤ Y) : have C := EulerNonlinearEnergyConstants.energyConstant period g0 g1 k B M Z0 B1 A0 A2 c; (g0 + g1 * X) * X + b * Y + k * forcingPolynomial period B M Z0 B0 B1 A0 A2 residual c Rc ρ X Y ≤ C * (X + X ^ 2 + residual) + (b + C * (ρ⁻¹ + Rc) * (B0 + X)) * Y

The existing polynomial growth constant absorbs the sharp drift forcing without replacing its small drift envelope by the full background envelope.

The actual correction forcing in metric energy with distinct full-background and small-drift budgets.

Sharp drift-preserving transport and pressure estimates for actual finite Sobolev fields.

Actual transport and pressure bounds retaining the small four-component drift norm.

theorem EulerDriftPreservingTransport.weightedCommutator_drift_smooth (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) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerSobolevTransportCommutator.weightedCommutatorNorm period hs N hN ρ L hL u v ≤ (EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Nonlinear.wordSobolevNorm period 6 n (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f)) * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v

The actual external commutator keeps the weighted norm of the four genuine drift components, including scale and tangency gains.

theorem EulerDriftPreservingTransport.transportPressure_shifted_drift_smooth (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s 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 : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (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) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : EulerGevreyPressureTransport.shiftedPressureNorm period N ρ (EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v) ≤ (4 * M * EulerH6Nonlinear.productConstant period 3 * ∑ n ∈ Finset.range (N + 2), EulerPacketWeights.weight ρ n * EulerH6Nonlinear.wordSobolevNorm period 6 n (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f)) * EulerSobolevTransportCommutator.weightedLoss period 6 (N + 1) ρ v

The actual shifted coercive pressure bound retains the weighted drift norm instead of replacing it by the full vector-field norm.

theorem EulerSobolevDriftTransport.weightedCommutator_drift_bound (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) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerSobolevTransportCommutator.weightedCommutatorNorm period hs N hN ρ L hL u v ≤ EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ * EulerSobolevDriftNorm.weightedDriftNorm period 6 N ρ (EulerFunctionalVelocity.velocityMap L) u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v

The genuine finite-Sobolev commutator retains the actual small drift norm in its radius-loss factor.

theorem EulerSobolevDriftTransport.transportPressure_shifted_drift (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s 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 : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (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) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerGevreyPressureTransport.shiftedPressureNorm period N ρ (EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v) ≤ 4 * M * EulerH6Nonlinear.productConstant period 3 * EulerSobolevDriftNorm.weightedDriftNorm period 6 (N + 1) ρ (EulerFunctionalVelocity.velocityMap L) u * EulerSobolevTransportCommutator.weightedLoss period 6 (N + 1) ρ v

The actual rough finite-Sobolev pressure estimate retains the small drift norm.

Actual nonlinear correction forcing with distinct full-velocity and drift factors.

theorem EulerDriftCorrectionForcing.nonlinear_externalPressure_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s 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 + 1 + 6 ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (EulerH6Pressure.CoefficientJet.restrict K 6 hs).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N + 1 → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerGevreyPressureEnergy.externalPressureNorm period K (N + 1) ρ (EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v) ≤ 8 * Rc * M * EulerH6Nonlinear.productConstant period 3 * EulerSobolevDriftNorm.weightedDriftNorm period 6 (N + 1) ρ (EulerFunctionalVelocity.velocityMap L) u * EulerSobolevTransportCommutator.weightedLoss period 6 (N + 1) ρ v

The nonlinear external pressure commutator keeps the actual drift norm at positive cutoff.

theorem EulerDriftCorrectionForcing.nonlinear_externalPressure_bound_all (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s 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 : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (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) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerGevreyPressureEnergy.externalPressureNorm period K N ρ (EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v) ≤ 8 * Rc * M * EulerH6Nonlinear.productConstant period 3 * EulerSobolevDriftNorm.weightedDriftNorm period 6 N ρ (EulerFunctionalVelocity.velocityMap L) u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v

The sharp external pressure bound also includes zero cutoff.

theorem EulerDriftCorrectionForcing.correctionForcing_raw_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) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f p0 p1 : ↥(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 p0 p1) ≤ EulerSobolevGevreyOperators.weightedNorm period 6 N ρ f + EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ * EulerSobolevDriftNorm.weightedDriftNorm period 6 N ρ (EulerFunctionalVelocity.velocityMap L) u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v + 5461 * EulerBaseTransportL2.baseTransportConstant period * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v + EulerGevreyPressureEnergy.externalPressureNorm period K N ρ p0 + EulerGevreyPressureEnergy.basePressureNorm period K0 N hN ρ p0 + EulerGevreyPressureEnergy.externalPressureNorm period K N ρ p1 + EulerGevreyPressureEnergy.basePressureNorm period K0 N hN ρ p1

Seven actual forcing arrays retain the sharp drift commutator factor.

theorem EulerDriftCorrectionForcing.correctionForcing_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 : ℝ) (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) (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)) ≤ (1 + 2 * M * (EulerSobolevGevreyOperators.weightedCoefficient period K 6 N ρ + 448 * EulerBasePressureCommutator.baseCoefficientSum period K0)) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ f + (5461 * EulerBaseTransportL2.baseTransportConstant period + 448 * EulerBasePressureCommutator.baseCoefficientSum period K0 * (8 * M * (5460 * EulerH6Nonlinear.lowerProductConstant period 3))) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v + (EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ + 8 * Rc * M * EulerH6Nonlinear.productConstant period 3) * EulerSobolevDriftNorm.weightedDriftNorm period 6 N ρ (EulerFunctionalVelocity.velocityMap L) u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v

The full actual forcing with both genuine projected pressure solves obeys the spatial part of equation (19). Every velocity derivative in the bound lies at or below the chosen cutoff.

theorem EulerDriftCorrectionForcing.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)) ≤ EulerGevreyCorrectionBound.sourceConstant B M * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ f + EulerGevreyCorrectionBound.transportConstant period B M * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v + (EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ + 8 * Rc * M * EulerH6Nonlinear.productConstant period 3) * EulerSobolevDriftNorm.weightedDriftNorm period 6 N ρ (EulerFunctionalVelocity.velocityMap L) u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v

Uniform fixed-base constants preserve the separate drift norm.

Actual nonlinear forcing with separate full-background and drift envelopes.

theorem EulerDriftNonlinearEstimate.drift_loss_absorption (P M Rc ρ B E Y D : ℝ) (hP : 0 ≤ P) (hM : 0 ≤ M) (hRc : 0 ≤ Rc) (hρ : 0 < ρ) (hB : 0 ≤ B) (hE : 0 ≤ E) (hY : 0 ≤ Y) (hD : D ≤ 4 * (B + E)) : (P * ρ⁻¹ + 8 * Rc * M * P) * D * Y ≤ (4 + 32 * M) * P * (ρ⁻¹ + Rc) * (B + E) * Y

The factor four is spent only on the correction drift, recovering the original uniform loss constant.

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

Scalar assembly keeps the independent full-velocity and drift envelopes in their respective terms.

theorem EulerDriftNonlinearEstimate.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)) (Z0 B0 B1 A0 A2 R : ℝ) (hA2 : 0 ≤ A2) (hz : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ z ≤ Z0) (hb : EulerSobolevDriftNorm.weightedDriftNorm period 6 N ρ (EulerFunctionalVelocity.velocityMap L) 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 * Z0) + EulerGevreyCorrectionBound.transportConstant period B M * Z0) * 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

The literal seven-term Euler forcing has a scalar bound preserving the actual small background drift.

theorem EulerDriftMetricForcing.correctionForcing_metric (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)) (Z0 B0 B1 A0 A2 R : ℝ) (hA2 : 0 ≤ A2) (hz : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ z ≤ Z0) (hb : EulerSobolevDriftNorm.weightedDriftNorm period 6 N ρ (EulerFunctionalVelocity.velocityMap L) 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) (KM : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (cM : ℝ) (hcM : 0 < cM) (hKM : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), cM ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (KM v) v) : 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)) ≤ EulerDriftEnergyConstants.forcingPolynomial period B M Z0 B0 B1 A0 A2 R cM Rc ρ (EulerGevreyMetricEstimate.energyNorm period N ⋯ ρ KM e) (EulerGevreyMetricEstimate.energyLoss period N ⋯ ρ KM e)

The genuine seven-term correction forcing obeys the metric polynomial retaining the small drift envelope.

Continuous energy majorants that retain the actual small transport drift.

noncomputable def EulerDriftEnergyMajorants.forcingMajorant (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerDriftCorrectionBudget.Budget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : C(↑(Set.Icc 0 T), ℝ)

The sharp polynomial is evaluated on the actual continuous metric energy paths.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerDriftEnergyMajorants.correctionRhs (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerDriftCorrectionBudget.Budget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (Rdot : C(↑(Set.Icc 0 T), ℝ)) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : C(↑(Set.Icc 0 T), ℝ)

The genuine scalar majorant retains full velocity only in terms with no derivative loss.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerDriftEnergyMajorants.correctionRhs_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerDriftCorrectionBudget.Budget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (Rdot : C(↑(Set.Icc 0 T), ℝ)) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (t : ↑(Set.Icc 0 T)) : have X := (EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) t; have Y := (EulerEnergyMetricPaths.lossPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) t; have C := EulerCorrectionEnergyMajorants.combinedConstant period S.full K; (correctionRhs period S hN K Rdot e) t ≤ C * (X + X ^ 2 + S.full.residual) + (Rdot t / R t + C * ((R t)⁻¹ + S.full.Rc) * (S.drift + X)) * Y

The source's radius-loss factor uses the drift envelope, with the unchanged full-data growth constant.

Actual nonlinear correction mild solutions obey the drift-sensitive integral energy estimate.

The actual time-dependent correction forcing obeys the sharp drift majorant.

theorem EulerDriftCorrectionEnergyBound.correctionArray_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerDriftCorrectionBudget.Budget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (V : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) (τ : ↑(Set.Icc 0 T)) (hV : (EulerCylinderSobolevSpace.truncateOperator period (q + 1)) V = e τ) : EulerWeightedCylinderEnergy.weightedForcingSum (R τ) (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (EulerCorrectionEnergyTime.correctionArray period hq D (EulerCorrectionEnergyData.baseMetricJet period hq D) N hN e V τ) ≤ (EulerDriftEnergyMajorants.forcingMajorant period S hN K e) τ

The actual correction array is controlled by the continuous drift majorant, independently of its auxiliary higher-Sobolev representative.

theorem EulerDriftCorrectionEnergyBound.weightedCorrectionForcing_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerDriftCorrectionBudget.Budget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => (D.metric.coefficient t).operator) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n e)) Filter.atTop (nhds U)) : ↑↑(EulerCorrectionEnergyTime.weightedCorrectionForcing period hq T hT D hG N hN R e U) ≤ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (EulerDriftEnergyMajorants.forcingMajorant period S hN K e)

The full Bochner forcing inherits the drift bound from the actual spatial fields.

theorem EulerDriftCorrectionMildEnergy.correction_mild_integral (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (KG : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.metric.coefficient t)) (KL : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.linear.coefficient t)) (KQ : (i : Fin 3) → (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q ((D.quadratic i).coefficient t)) (hGq : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t)) (hLq : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t)) (hQq : ∀ (i : Fin 3), Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t)) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => (D.metric.coefficient t).operator) (N : ℕ) (hN : N + 6 ≤ q + 1) (R Rdot : C(↑(Set.Icc 0 T), ℝ)) (S : EulerDriftCorrectionBudget.Budget period ⋯ D N R) (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (hRd : ∀ t ∈ Set.Ioo 0 T, HasDerivAt (EulerVolterraConvolution.extendPath T hT R) (EulerVolterraConvolution.extendPath T hT Rdot t) t) (ν : ℝ) (hν : 0 < ν) (hν1 : ν ≤ 1) (e₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), e t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) e₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT (EulerCorrectionLowerData.forcingPath period hq (EulerCorrectionLowerData.lowerData period D KG KL KQ hGq hLq hQq) e) (↑t - r))) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (he : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) : (EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) ⟨t, ⋯⟩ - (EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) ⟨s, ⋯⟩ ≤ ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT (EulerDriftEnergyMajorants.correctionRhs period S hN K Rdot e) r

The actual nonlinear lower mild equation yields the full energy-order scalar integral bound on every subinterval. Maximal regularity, the higher nonlinear source, the pressure, and their constraints are all constructed or proved inside the argument.

theorem EulerDriftCorrectionBootstrap.correction_mild_bootstrap (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (KG : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.metric.coefficient t)) (KL : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.linear.coefficient t)) (KQ : (i : Fin 3) → (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q ((D.quadratic i).coefficient t)) (hGq : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t)) (hLq : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t)) (hQq : ∀ (i : Fin 3), Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t)) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => (D.metric.coefficient t).operator) (N : ℕ) (hN : N + 6 ≤ q + 1) (R Rdot : C(↑(Set.Icc 0 T), ℝ)) (S : EulerDriftCorrectionBudget.Budget period ⋯ D N R) (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (C Δ ρ0 : ℝ) (hC : EulerCorrectionEnergyMajorants.combinedConstant period S.full K ≤ C) (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1) (hρ0 : 0 < ρ0) (hdecay : 2 * C * (S.drift + Δ) * T ≤ ρ0 / 2) (hscale : ρ0 * S.full.Rc ≤ 1) (hsmall : 2 * S.full.residual * Real.exp (3 * C * T) ≤ Δ / 2) (hR : ∀ (t : ↑(Set.Icc 0 T)), R t = ρ0 - 2 * C * (S.drift + Δ) * ↑t) (hRdot : ∀ (t : ↑(Set.Icc 0 T)), Rdot t = -2 * C * (S.drift + Δ)) (ν : ℝ) (hν : 0 < ν) (hν1 : ν ≤ 1) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), e t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) 0 + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT (EulerCorrectionLowerData.forcingPath period hq (EulerCorrectionLowerData.lowerData period D KG KL KQ hGq hLq hQq) e) (↑t - r))) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (he : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (t : ↑(Set.Icc 0 T)) : EulerGevreyMetricEstimate.energyNorm period N hN (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) (e t) ≤ 2 * S.full.residual * Real.exp (3 * C * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period N hN (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) (e t) ≤ Δ / 2

Every actual zero-initial nonlinear correction mild solution satisfies the closed Gevrey estimate. The proof derives its full-order all-subinterval energy inequality, source bound, pressure cancellation, and maximal regularity rather than assuming them.