Fixed, actual coefficient budgets for L² viscosity stability.

noncomputable def EulerCorrectionStabilityConstants.lowerConstant (period : ℝ) [Fact (0 < period)] (q : ℕ) (A0 A2 Z R : ℝ) : ℝ

The fixed L² Lipschitz coefficient of all non-top-transport difference terms.

Equations

• EulerCorrectionStabilityConstants.lowerConstant period q A0 A2 Z R = A0 + (4 + 2 * A2) * EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * (Z + R)

noncomputable def EulerCorrectionStabilityConstants.velocityBound (period : ℝ) [Fact (0 < period)] (q : ℕ) (Z R : ℝ) : ℝ

A fixed pointwise bound for the actual background-plus-error advecting velocity.

Equations

• EulerCorrectionStabilityConstants.velocityBound period q Z R = EulerCylinderSobolevSpace.sobolevEmbeddingConstant period q * (Z + R)

noncomputable def EulerCorrectionStabilityConstants.growthConstant (c Kb Kx Kt V L : ℝ) : ℝ

The squared-metric growth coefficient after the genuine transport and heat cancellations.

Equations

• EulerCorrectionStabilityConstants.growthConstant c Kb Kx Kt V L = (Kt + 2 * Kx * V + 4 * Kx ^ 2 / c ^ 2 + 2 * Kb * L + 1) / c ^ 2

def EulerCorrectionStabilityConstants.defectConstant (Kb R : ℝ) : ℝ

The fixed coefficient of the squared viscosity difference.

Equations

• EulerCorrectionStabilityConstants.defectConstant Kb R = (Kb * (4 * R)) ^ 2

theorem EulerCorrectionStabilityConstants.lowerConstant_nonneg (period : ℝ) [Fact (0 < period)] (q : ℕ) (A0 A2 Z R : ℝ) (hA0 : 0 ≤ A0) (hA2 : 0 ≤ A2) (hZ : 0 ≤ Z) (hR : 0 ≤ R) : 0 ≤ lowerConstant period q A0 A2 Z R

Nonnegative actual coefficient and norm budgets give a nonnegative lower-order Lipschitz constant.

theorem EulerCorrectionStabilityConstants.velocityBound_nonneg (period : ℝ) [Fact (0 < period)] (q : ℕ) (Z R : ℝ) (hZ : 0 ≤ Z) (hR : 0 ≤ R) : 0 ≤ velocityBound period q Z R

The actual pointwise velocity budget is nonnegative.

theorem EulerCorrectionStabilityConstants.differenceRemainder_uniform (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period q T) (hq : 6 ≤ q) (t : T) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (A0 A2 Z R : ℝ) (hA0 : ↑(D.linear.coefficient t).bound ≤ A0) (hA2 : ∑ i : Fin 3, ↑((D.quadratic i).coefficient t).bound ≤ A2) (hZ : ‖D.approximation t‖ ≤ Z) (hu : ‖u‖ ≤ R) (hv : ‖v‖ ≤ R) : ‖EulerCylinderSobolevSpace.value period (EulerCorrectionDifference.differenceRemainder period D hq t u v)‖ ≤ lowerConstant period q A0 A2 Z R * ‖EulerCylinderSobolevSpace.value period (u - v)‖

Actual higher Sobolev and coefficient bounds give the lower-order difference estimate in L².

theorem EulerCorrectionStabilityConstants.growthConstant_nonneg (c Kb Kx Kt V L : ℝ) (hKb : 0 ≤ Kb) (hKx : 0 ≤ Kx) (hKt : 0 ≤ Kt) (hV : 0 ≤ V) (hL : 0 ≤ L) : 0 ≤ growthConstant c Kb Kx Kt V L

The actual fixed growth coefficient is nonnegative.