The already-proved Gevrey budgets supply every actual vanishing-viscosity stability budget.

theorem EulerGevreyStabilityBudget.coefficient_bound_le_block (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) : ↑A.bound ≤ EulerH6Pressure.coefficientBlock period K 6 0

The actual uniform coefficient bound is contained in its fixed H6 coefficient block.

theorem EulerGevreyStabilityBudget.coefficient_bound_le_weighted (period : ℝ) {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) : ↑A.bound ≤ EulerSobolevGevreyOperators.weightedCoefficient period K 6 N ρ

The actual uniform coefficient bound is contained in every positive-radius truncated Gevrey coefficient sum.

def EulerGevreyStabilityBudget.stabilityBudgetLower (period : ℝ) [Fact (0 < period)] {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)) (N : ℕ) (R : C(↑(Set.Icc 0 T), ℝ)) (hq : 6 ≤ q + 1) (B : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (K : EulerCorrectionEnergyData.MetricBudget period T hT D) : EulerCorrectionStabilityBudget.StabilityBudget period hT (EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ)

The concrete global Gevrey and metric budgets directly construct the viscosity comparison budget on the genuine lower equation.

Equations

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