Actual all-order Gevrey input budgets with radius loss controlled by the transport drift.

structure EulerAllOrderDriftCorrection.Budget (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) : Type

Genuine coherent input budgets for the drift-aware all-order correction theorem. Full background norms enter the proved polynomial constants; only the actual transport drift enters the shrinking-radius slope.

• metric : EulerCorrectionEnergyData.MetricBudget period T ⋯ (EulerAllOrderCorrectionData.Data.atOrder period A 1)

  The actual common inverse metric and its genuine time derivative.

• radius : C(↑(Set.Icc 0 T), ℝ)

  The common positive shrinking radius.

• growthCoefficient : ℝ

  The common scalar dominating the proved nonlinear growth constants.

• delta : ℝ

  The desired common correction bound.

• initialRadius : ℝ

  The common initial radius.

• spatial (q : ℕ) (hq : 6 ≤ q) : EulerDriftCorrectionBudget.Budget period ⋯ (EulerAllOrderCorrectionData.Data.atOrder period A (q + 1 + 1)) (q - 4) self.radius

  Actual coefficient, full-velocity, drift and residual bounds at every construction order.

• growth_bound (q : ℕ) (hq : 6 ≤ q) : EulerCorrectionEnergyMajorants.combinedConstant period (self.spatial q hq).full (EulerAllOrderCorrectionData.Data.metricBudget period A ⋯ self.metric (q + 1)) ≤ self.growthCoefficient

  The common scalar bounds each actual proved energy constant.

• delta_pos : 0 < self.delta

  The target error is strictly positive.

• delta_le_one : self.delta ≤ 1

  The target error is at most one.

• radius_pos : 0 < self.initialRadius

  The initial radius is strictly positive.

• decay (q : ℕ) (hq : 6 ≤ q) : 2 * self.growthCoefficient * ((self.spatial q hq).drift + self.delta) * T ≤ self.initialRadius / 2

  The actual drift permits retention of half of the initial radius.

• scale (q : ℕ) (hq : 6 ≤ q) : self.initialRadius * (self.spatial q hq).full.Rc ≤ 1

  The coefficient scale fits the initial radius.

• small (q : ℕ) (hq : 6 ≤ q) : 2 * (self.spatial q hq).full.residual * Real.exp (3 * self.growthCoefficient * T) ≤ self.delta / 2

  The actual residual bound beats the genuine Gronwall factor.

• radius_eq (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : self.radius t = self.initialRadius - 2 * self.growthCoefficient * ((self.spatial q hq).drift + self.delta) * ↑t

  The same actual radius is used at every order, with slope determined by the drift envelope.

• divergence (t : ↑(Set.Icc 0 T)) : A.approximation.field t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction

  The prescribed approximation satisfies the actual lifted divergence constraint.

def EulerAllOrderDriftCorrection.Budget.comparisonData (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : EulerCorrectionAssembly.ComparisonData period hT A

The drift-aware input budget provides the genuine comparison data required by finite-order uniqueness.

Equations

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