Related estimates used together by the same construction modules.

The constructed higher nonlinear source and pressure restrict exactly to the actual lower mild equation.

theorem EulerCorrectionEnergyRestriction.rawTime_restriction (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)) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t)) (hL : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t)) (hQ : ∀ (i : Fin 3), Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t)) (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)) : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑(EulerCorrectionEnergyTime.rawTime period ⋯ T hT D e U) t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (EulerCorrectionLowerData.rawPath period hq (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) e)

The actual higher raw nonlinear time field restricts to the actual continuous source of the lower equation.

theorem EulerCorrectionEnergyRestriction.sourceTime_restriction (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)) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t)) (hL : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t)) (hQ : ∀ (i : Fin 3), Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t)) (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)) : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑(EulerCorrectionEnergyTime.sourceTime period ⋯ T hT D e U) t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (EulerCorrectionLowerData.forcingPath period hq (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) e)

The actual full-order projected time forcing restricts to the literal lower mild source without a source-regularity premise.

theorem EulerCorrectionEnergyRestriction.signedPressureTime_restriction (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)) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t)) (hL : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t)) (hQ : ∀ (i : Fin 3), Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t)) (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)) : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑(EulerCorrectionEnergyTime.signedPressureTime period ⋯ T hT D e U) t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (EulerCorrectionLowerData.pressurePath period hq (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) e)

The actual full-order signed pressure restricts exactly to the continuous pressure in the lower correction equation.

Full energy-order signed Gevrey bounds from genuine viscous mild solutions with continuous scalar coefficient majorants.

Actual finite-Sobolev viscous PDE energy with continuous scalar majorants, requiring no measurability of coefficient-bound witnesses.

theorem EulerWeightedSobolevMajorant.weighted_sobolev_energy_majorized (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (hq : 3 ≤ q) (order : α → ℕ) (ρ ρ' : ℝ → ℝ) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K G : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period) (e : α → β → ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) (e' p forcing : α → β → ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (z : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (s t c ν : ℝ) (K' : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (B : ℝ → NNReal) (growth multiplier : ℝ → ℝ) (hst : s ≤ t) (hc : 0 < c) (hν : 0 ≤ ν) (hgrowth : ∀ u ∈ Set.Ioo s t, EulerWeightedCylinderEnergy.viscousGrowthCoefficient period (K u) (K' u) κ m c ν (B u) ≤ growth u) (hmultiplier : ∀ u ∈ Set.Ioo s t, ↑(K u).bound / c ≤ multiplier u) (hρc : ContinuousOn ρ (Set.Icc s t)) (hρpos : ∀ u ∈ Set.Icc s t, 0 < ρ u) (hρd : ∀ u ∈ Set.Ioo s t, HasDerivAt ρ (ρ' u) u) (hKc : ContinuousOn (fun (u : ℝ) => (K u).operator) (Set.Icc s t)) (hec : ∀ (i : α) (j : β), ContinuousOn (fun (u : ℝ) => EulerCylinderSobolevSpace.value period (e i j u)) (Set.Icc s t)) (hKt : ∀ u ∈ Set.Ioo s t, HasDerivAt (fun (v : ℝ) => (K v).operator) (K' u) u) (het : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, HasDerivAt (fun (v : ℝ) => EulerCylinderSobolevSpace.value period (e i j v)) (e' i j u) u) (hsym : ∀ u ∈ Set.Ioo s t, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ (((K u).coefficient x) v) w = inner ℝ v (((K u).coefficient x) w)) (hpos : ∀ u ∈ Set.Icc s t, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (((K u).coefficient x) v) v) (hKG : ∀ u ∈ Set.Ioo s t, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), ((K u).coefficient x) (((G u).coefficient x) v) = v) (hediv : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, EulerCylinderSobolevSpace.value period (e i j u) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hp : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, p i j u ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (hz : ∀ u ∈ Set.Ioo s t, EulerCylinderSobolevSpace.value period (z u) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hzB : ∀ u ∈ Set.Ioo s t, ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period (z u)) x‖ ≤ ↑(B u)) (heq : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, e' i j u + (EulerSobolevMetricTransport.transportOperator period hq κ m (z u)) ((EulerCylinderSobolevSpace.restrictOperator period weighted_sobolev_energy_majorized._proof_1) (e i j u)) + (G u).operator (p i j u) = forcing i j u + ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period (e i j u))) (hAint : ∀ (i : α), MeasureTheory.IntegrableOn (fun (u : ℝ) => EulerPacketWeights.weight (ρ u) (order i) * growth u + ρ' u / ρ u * ↑(order i) * EulerPacketWeights.weight (ρ u) (order i)) (Set.Icc s t) MeasureTheory.volume) (hFint : ∀ (i : α), MeasureTheory.IntegrableOn (fun (u : ℝ) => EulerPacketWeights.weight (ρ u) (order i) * (multiplier u * EulerFiniteMetricEnergy.familyNorm fun (j : β) => forcing i j u)) (Set.Icc s t) MeasureTheory.volume) : ((EulerWeightedCylinderEnergy.weightedMetricSum (ρ t) order (K t).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e i j t)) - EulerWeightedCylinderEnergy.weightedMetricSum (ρ s) order (K s).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e i j s)) ≤ ∫ (u : ℝ) in s..t, ((growth u * EulerWeightedCylinderEnergy.weightedMetricSum (ρ u) order (K u).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e i j u)) + ρ' u / ρ u * EulerWeightedCylinderEnergy.weightedMetricLoss (ρ u) order (K u).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e i j u)) + multiplier u * EulerWeightedCylinderEnergy.weightedForcingSum (ρ u) order fun (i : α) (j : β) => forcing i j u

Continuous scalar majorants give the finite Gevrey integral inequality directly from the actual viscous PDE. The signed radius term is retained exactly, and no differentiability of the unregularized norm is assumed.

Actual PDE energy passage with continuous scalar majorants on every time subinterval.

theorem EulerPDEMajorantLimit.weighted_pde_majorized_subinterval_limit (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (hq : 3 ≤ q) (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) (order : α → ℕ) (a b d : C(↑(Set.Icc 0 T), ℝ)) (ρ ρ' : ℝ → ℝ) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K G : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period) (e : ℕ → α → β → ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) (e' p forcing : ℕ → α → β → ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (z : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (c ν : ℝ) (K' : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (B : ℝ → NNReal) (hc : 0 < c) (hν : 0 ≤ ν) (hρc : ContinuousOn ρ (Set.Icc 0 T)) (hρpos : ∀ r ∈ Set.Icc 0 T, 0 < ρ r) (hρd : ∀ r ∈ Set.Ioo 0 T, HasDerivAt ρ (ρ' r) r) (hKc : ContinuousOn (fun (r : ℝ) => (K r).operator) (Set.Icc 0 T)) (hec : ∀ (n : ℕ) (i : α) (j : β), ContinuousOn (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (e n i j r)) (Set.Icc 0 T)) (hKt : ∀ r ∈ Set.Ioo 0 T, HasDerivAt (fun (v : ℝ) => (K v).operator) (K' r) r) (het : ∀ (n : ℕ) (i : α) (j : β), ∀ r ∈ Set.Ioo 0 T, HasDerivAt (fun (v : ℝ) => EulerCylinderSobolevSpace.value period (e n i j v)) (e' n i j r) r) (hsym : ∀ r ∈ Set.Ioo 0 T, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ (((K r).coefficient x) v) w = inner ℝ v (((K r).coefficient x) w)) (hpos : ∀ r ∈ Set.Icc 0 T, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (((K r).coefficient x) v) v) (hKG : ∀ r ∈ Set.Ioo 0 T, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), ((K r).coefficient x) (((G r).coefficient x) v) = v) (hediv : ∀ (n : ℕ) (i : α) (j : β), ∀ r ∈ Set.Ioo 0 T, EulerCylinderSobolevSpace.value period (e n i j r) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hp : ∀ (n : ℕ) (i : α) (j : β), ∀ r ∈ Set.Ioo 0 T, p n i j r ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (hz : ∀ r ∈ Set.Ioo 0 T, EulerCylinderSobolevSpace.value period (z r) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hzB : ∀ r ∈ Set.Ioo 0 T, ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period (z r)) x‖ ≤ ↑(B r)) (heq : ∀ (n : ℕ) (i : α) (j : β), ∀ r ∈ Set.Ioo 0 T, e' n i j r + (EulerSobolevMetricTransport.transportOperator period hq κ m (z r)) ((EulerCylinderSobolevSpace.restrictOperator period EulerWeightedSobolevMajorant.weighted_sobolev_energy_majorized._proof_1) (e n i j r)) + (G r).operator (p n i j r) = forcing n i j r + ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period (e n i j r))) (hAint : ∀ (i : α), MeasureTheory.IntegrableOn (fun (r : ℝ) => EulerPacketWeights.weight (ρ r) (order i) * EulerVolterraConvolution.extendPath T hT a r + ρ' r / ρ r * ↑(order i) * EulerPacketWeights.weight (ρ r) (order i)) (Set.Icc 0 T) MeasureTheory.volume) (hFint : ∀ (n : ℕ) (i : α), MeasureTheory.IntegrableOn (fun (r : ℝ) => EulerPacketWeights.weight (ρ r) (order i) * (EulerVolterraConvolution.extendPath T hT d r * EulerFiniteMetricEnergy.familyNorm fun (j : β) => forcing n i j r)) (Set.Icc 0 T) MeasureTheory.volume) (ha : ∀ r ∈ Set.Icc 0 T, EulerWeightedCylinderEnergy.viscousGrowthCoefficient period (K r) (K' r) κ m c ν (B r) ≤ EulerVolterraConvolution.extendPath T hT a r) (hb : ∀ r ∈ Set.Icc 0 T, ρ' r / ρ r = EulerVolterraConvolution.extendPath T hT b r) (hd : ∀ r ∈ Set.Icc 0 T, ↑(K r).bound / c ≤ EulerVolterraConvolution.extendPath T hT d r) (X Y Z : ℕ → C(↑(Set.Icc 0 T), ℝ)) (hXdef : ∀ (n : ℕ), ∀ r ∈ Set.Icc 0 T, (EulerWeightedCylinderEnergy.weightedMetricSum (ρ r) order (K r).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e n i j r)) = EulerVolterraConvolution.extendPath T hT (X n) r) (hYdef : ∀ (n : ℕ), ∀ r ∈ Set.Icc 0 T, (EulerWeightedCylinderEnergy.weightedMetricLoss (ρ r) order (K r).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e n i j r)) = EulerVolterraConvolution.extendPath T hT (Y n) r) (hZdef : ∀ (n : ℕ), ∀ r ∈ Set.Icc 0 T, (EulerWeightedCylinderEnergy.weightedForcingSum (ρ r) order fun (i : α) (j : β) => forcing n i j r) = EulerVolterraConvolution.extendPath T hT (Z n) r) (x y : C(↑(Set.Icc 0 T), ℝ)) (f : ↥(EulerTimeLp.TimeLp T ℝ)) (hX : Filter.Tendsto X Filter.atTop (nhds x)) (hY : Filter.Tendsto Y Filter.atTop (nhds y)) (hZ : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (Z n)) Filter.atTop (nhds f)) : x ⟨t, ⋯⟩ - x ⟨s, ⋯⟩ ≤ ((∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT x r) + ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT b r * EulerVolterraConvolution.extendPath T hT y r) + ∫ (r : ℝ) in Set.Icc s t, ↑↑(EulerTimeLp.pathLp T hT d) r * ↑↑f r ∂EulerTimeLp.timeMeasure T

Actual smooth-in-time finite-Sobolev PDE approximations imply the limiting signed integral energy bound. The premises include their literal PDEs and strong convergence, never an assumed energy inequality.

theorem EulerMildMajorantEnergy.mild_majorized_energy_subinterval (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (hq : 3 ≤ q + 1) (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hw : ∀ (i : α) (j : β), d i j ≤ q + 1) (order : α → ℕ) (ν : ℝ) (hν : 0 < ν) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (R Rdot : C(↑(Set.Icc 0 T), ℝ)) (hR : ∀ (r : ↑(Set.Icc 0 T)), 0 < R r) (hRd : ∀ r ∈ Set.Ioo 0 T, HasDerivAt (EulerVolterraConvolution.extendPath T hT R) (EulerVolterraConvolution.extendPath T hT Rdot r) r) (K G : ↑(Set.Icc 0 T) → EulerSpatialSobolevInverse.SmoothCoefficient period) (hK : Continuous fun (r : ↑(Set.Icc 0 T)) => (K r).operator) (hG : Continuous fun (r : ↑(Set.Icc 0 T)) => (G r).operator) (Kdot : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (hKd : ∀ r ∈ Set.Ioo 0 T, HasDerivAt (EulerVolterraConvolution.extendPath T hT (EulerRegularizedMetricPaths.metricOperatorPath period T K hK)) (EulerVolterraConvolution.extendPath T hT Kdot r) r) (hKsym : ∀ (r : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v v' : EulerLiftedGradientSpace.Vector3), inner ℝ (((K r).coefficient x) v) v' = inner ℝ v (((K r).coefficient x) v')) (hKpos : ∀ (r : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (((K r).coefficient x) v) v) (hKG : ∀ (r : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), ((K r).coefficient x) (((G r).coefficient x) v) = v) (B : ↑(Set.Icc 0 T) → NNReal) (z u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (hsol : ∀ (r : ↑(Set.Icc 0 T)), u r = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑r).toNNReal) u₀ + ∫ (v : ℝ) in 0..↑r, (EulerSobolevHeat.heatKernel period q ν hν v) (EulerVolterraConvolution.extendPath T hT f (↑r - v))) (hu : ∀ (r : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (u r) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hp : ∀ (r : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (p r) ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (hz : ∀ (r : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (z r) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hzB : ∀ (r : ↑(Set.Icc 0 T)), ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period (z r)) x‖ ≤ ↑(B r)) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)) Filter.atTop (nhds U)) (hF : (fun (r : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑F r)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT f) (hP : (fun (r : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑P r)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT p) (a b k : C(↑(Set.Icc 0 T), ℝ)) (ha : ∀ (r : ↑(Set.Icc 0 T)), EulerWeightedCylinderEnergy.viscousGrowthCoefficient period (K r) (Kdot r) κ m c ν (B r) ≤ a r) (hb : ∀ (r : ↑(Set.Icc 0 T)), Rdot r / R r = b r) (hk : ∀ (r : ↑(Set.Icc 0 T)), ↑(K r).bound / c ≤ k r) : have A := EulerTransportL2Time.transportL2Path period hq κ m T z; have Kp := EulerRegularizedMetricPaths.metricOperatorPath period T K hK; have Gp := EulerRegularizedMetricPaths.metricOperatorPath period T G hG; have weights := fun (i : α) => EulerSobolevEnergyPaths.gevreyWeightPath T R (order i); have x := EulerMetricPathConvergence.weightedMetricPath T weights Kp (EulerRegularizedEnergyFamily.energyValueFamily period d w hw T u); have y := EulerMetricPathConvergence.weightedMetricPath T (fun (i : α) => EulerSobolevEnergyPaths.gevreyLossWeightPath T R (order i)) Kp (EulerRegularizedEnergyFamily.energyValueFamily period d w hw T u); have Z := EulerWeightedForcingTime.weightedForcingTime T hT weights (EulerRegularizedEnergyFamily.forcingFamilyTime period d w hw T hT A Gp U F P); x ⟨t, ⋯⟩ - x ⟨s, ⋯⟩ ≤ ((∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT x r) + ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT b r * EulerVolterraConvolution.extendPath T hT y r) + ∫ (r : ℝ) in Set.Icc s t, ↑↑(EulerTimeLp.pathLp T hT k) r * ↑↑Z r ∂EulerTimeLp.timeMeasure T

Every full-order finite Gevrey word family of an actual viscous mild solution obeys the signed integral estimate with continuous scalar majorants on every subinterval. The derivative and forcing limits are obtained from actual heat regularization; no energy inequality or differentiability of a zero norm is assumed.