Concrete coefficient and inverse-metric data for actual vanishing-viscosity stability.

structure EulerCorrectionStabilityBudget.StabilityBudget (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)) : Type

Actual coefficient and inverse-metric budgets for L² comparison; no PDE estimate or solution comparison is a field.

• metric : ↑(Set.Icc 0 T) → EulerSpatialSobolevInverse.SmoothCoefficient period

  The actual inverse metric coefficient.

• continuous : Continuous fun (t : ↑(Set.Icc 0 T)) => (self.metric t).operator

  The actual metric multiplier is continuous in time.

• derivative : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))

  The genuine time derivative of the metric multiplier.

• hasDeriv (t : ℝ) : t ∈ Set.Ioo 0 T → HasDerivAt (fun (s : ℝ) => (self.metric (Set.projIcc 0 T hT s)).operator) (EulerVolterraConvolution.extendPath T hT self.derivative t) t

  Interior differentiation of the actual metric path.

• c : ℝ

  Positive square-root coercivity constant.

• c_pos : 0 < self.c

  Strict coercivity.

• symmetric (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (a b : EulerLiftedGradientSpace.Vector3) : inner ℝ (((self.metric t).coefficient x) a) b = inner ℝ a (((self.metric t).coefficient x) b)

  Pointwise metric symmetry.

• coercive (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (a : EulerLiftedGradientSpace.Vector3) : self.c ^ 2 * ‖a‖ ^ 2 ≤ inner ℝ (((self.metric t).coefficient x) a) a

  Pointwise positive lower bound.

• inverse (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (a : EulerLiftedGradientSpace.Vector3) : ((self.metric t).coefficient x) (((D.metric.coefficient t).coefficient x) a) = a

  The actual metric inverts the pressure coefficient.

• bound : ℝ

  Uniform metric operator bound.

• first : ℝ

  Uniform metric first spatial derivative bound.

• time : ℝ

  Uniform metric time derivative bound.

• linear : ℝ

  Uniform linear-coefficient bound.

• quadratic : ℝ

  Uniform sum of quadratic-coefficient bounds.

• bound_le (t : ↑(Set.Icc 0 T)) : ‖(self.metric t).operator‖ ≤ self.bound

  The actual metric operator satisfies its budget.

• first_le (t : ↑(Set.Icc 0 T)) : ↑(self.metric t).firstBound ≤ self.first

  The actual first spatial derivative witness satisfies its budget.

• time_le (t : ↑(Set.Icc 0 T)) : ‖self.derivative t‖ ≤ self.time

  The actual time derivative satisfies its budget.

• linear_le (t : ↑(Set.Icc 0 T)) : ↑(D.linear.coefficient t).bound ≤ self.linear

  The actual linear coefficient satisfies its budget.

• quadratic_le (t : ↑(Set.Icc 0 T)) : ∑ i : Fin 3, ↑((D.quadratic i).coefficient t).bound ≤ self.quadratic

  The actual quadratic coefficients satisfy their common budget.

noncomputable def EulerCorrectionStabilityBudget.StabilityBudget.operatorPath (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)} (B : StabilityBudget period hT D) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))

The actual continuous metric multiplier path determined by the concrete budget.

Equations

• EulerCorrectionStabilityBudget.StabilityBudget.operatorPath period B = { toFun := fun (t : ↑(Set.Icc 0 T)) => (B.metric t).operator, continuous_toFun := ⋯ }

noncomputable def EulerCorrectionStabilityBudget.StabilityBudget.growth (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)} (B : StabilityBudget period hT D) (R : ℝ) : ℝ

The fixed squared-energy growth coefficient obtained from the actual background path and a solution norm bound.

Equations

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

noncomputable def EulerCorrectionStabilityBudget.StabilityBudget.comparisonConstant (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)} (B : StabilityBudget period hT D) (R : ℝ) : ℝ

The explicit finite-interval Lipschitz coefficient for viscosity in continuous L².

Equations

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

theorem EulerCorrectionStabilityBudget.StabilityBudget.nonneg (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)} (B : StabilityBudget period hT D) : 0 ≤ B.bound ∧ 0 ≤ B.first ∧ 0 ≤ B.time ∧ 0 ≤ B.linear ∧ 0 ≤ B.quadratic

All budget signs follow from the actual norm bounds on the nonempty time interval.

theorem EulerCorrectionStabilityBudget.StabilityBudget.growth_nonneg (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)} (B : StabilityBudget period hT D) (R : ℝ) (hR : 0 ≤ R) : 0 ≤ growth period B R

The actual fixed growth coefficient is nonnegative for every nonnegative solution bound.

theorem EulerCorrectionStabilityBudget.StabilityBudget.comparisonConstant_nonneg (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hT : 0 ≤ T} {D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)} (B : StabilityBudget period hT D) (R : ℝ) : 0 ≤ comparisonConstant period B R

The explicit comparison coefficient is nonnegative.