Actual metric-energy growth coefficients bounded uniformly for artificial viscosities at most one.

noncomputable def EulerGevreyGrowthCoefficient.growthBase (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (c : ℝ) : ℝ

The viscosity-uniform constant part of the actual metric growth coefficient.

Equations

• EulerGevreyGrowthCoefficient.growthBase period K K' c = (‖K'‖ + 2 * EulerCylinderViscousEnergy.heatEnergyConstant period K c) / (2 * c ^ 2)

noncomputable def EulerGevreyGrowthCoefficient.growthSlope (period : ℝ) (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) : ℝ

The exact slope of the actual metric growth coefficient with respect to the velocity bound.

Equations

• EulerGevreyGrowthCoefficient.growthSlope period K κ m c = ↑K.firstBound * (|κ| + ‖m‖) / (2 * c ^ 2)

theorem EulerGevreyGrowthCoefficient.growthBase_nonneg (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (c : ℝ) : 0 ≤ growthBase period K K' c

theorem EulerGevreyGrowthCoefficient.growthSlope_nonneg (period : ℝ) (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) : 0 ≤ growthSlope period K κ m c

theorem EulerGevreyGrowthCoefficient.viscousGrowth_uniform (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c ν : ℝ) (B : NNReal) (hν : ν ≤ 1) : EulerWeightedCylinderEnergy.viscousGrowthCoefficient period K K' κ m c ν B ≤ growthBase period K K' c + growthSlope period K κ m c * ↑B

Artificial viscosity contributes no unbounded constant to the actual energy estimate as it tends to zero.

theorem EulerGevreyGrowthCoefficient.metricVelocityBound_continuous (period : ℝ) [Fact (0 < period)] (c B : ℝ) : Continuous (EulerGevreyMetricEstimate.metricVelocityBound period c B)

The chosen genuine pointwise velocity bound depends continuously on the actual metric energy.

theorem EulerGevreyGrowthCoefficient.metricVelocityBound_coe (period : ℝ) [Fact (0 < period)] (c B X : ℝ) (hc : 0 < c) (hB : 0 ≤ B) (hX : 0 ≤ X) : ↑(EulerGevreyMetricEstimate.metricVelocityBound period c B X) = EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 6 * (B + EulerGevreyMetricEstimate.metricAmplification c * X)

Its NNReal coercion is exactly the intended positive metric-energy majorant.

theorem EulerGevreyGrowthCoefficient.viscousGrowth_metric (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c ν B X : ℝ) (hc : 0 < c) (hν : ν ≤ 1) (hB : 0 ≤ B) (hX : 0 ≤ X) : EulerWeightedCylinderEnergy.viscousGrowthCoefficient period K K' κ m c ν (EulerGevreyMetricEstimate.metricVelocityBound period c B X) ≤ growthBase period K K' c + growthSlope period K κ m c * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 6 * B + growthSlope period K κ m c * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 6 * EulerGevreyMetricEstimate.metricAmplification c * X

The actual energy growth coefficient is affine in the metric error energy, uniformly for 0<ν≤1.

theorem EulerGevreyGrowthCoefficient.absorb_scalar_coefficients (g0 g1 f0 f1 f2 d r X Y B R C : ℝ) (hg0 : 0 ≤ g0) (hg1 : 0 ≤ g1) (hf0 : 0 ≤ f0) (hf1 : 0 ≤ f1) (hf2 : 0 ≤ f2) (hd : 0 ≤ d) (hr : 0 ≤ r) (hX : 0 ≤ X) (hY : 0 ≤ Y) (hB : 0 ≤ B) (hR : 0 ≤ R) (hC : 1 + g0 + g1 + f0 + f1 + f2 + d ≤ C) (b : ℝ) : (g0 + g1 * X) * X + b * Y + (f0 * r + f1 * X + f2 * X ^ 2 + d * R * (B + X) * Y) ≤ C * (X + X ^ 2 + r) + (b + C * R * (B + X)) * Y

One positive constant absorbs every derived scalar growth coefficient while preserving the signed radius term.