Genuine correction data with separate full-velocity and transport-drift bounds.
structure
EulerDriftCorrectionBudget.Budget
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : ℝ}
(hq : 6 ≤ q + 1)
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(N : ℕ)
(R : C(↑(Set.Icc 0 T), ℝ))
:
The full coefficient budget is retained, while the actual small drift has its own envelope.
- full : EulerCorrectionEnergyData.SpatialBudget period hq D N R
All full-velocity and coefficient norms, including the residual, are actual data bounds.
- drift : ℝ
The smaller bound used in the shrinking-radius slope.
A norm envelope is nonnegative.
- drift_bound (t : ↑(Set.Icc 0 T)) : EulerSobolevDriftNorm.weightedDriftNorm period 6 N (R t) (EulerFunctionalVelocity.velocityMap (EulerSobolevTransport.velocityComponents D.κ D.direction)) (D.approximation t) ≤ self.drift
The weighted norm of the actual four-component background drift.
Instances For
def
EulerDriftCorrectionBudget.Budget.restrict
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T S : ℝ}
{hq : 6 ≤ q + 1}
{D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 S)}
{N : ℕ}
{R : C(↑(Set.Icc 0 S), ℝ)}
(B : Budget period hq D N R)
(hTS : T ≤ S)
:
Budget period hq (EulerCorrectionOperators.CorrectionData.comp period D (EulerQuadraticSource.timeInclusion hTS)) N
(R.comp (EulerQuadraticSource.timeInclusion hTS))
Restricting the time interval preserves both actual norm bounds and all constants.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerDriftCorrectionBudget.Budget.total_drift_bound
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : ℝ}
{hq : 6 ≤ q + 1}
{D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)}
{N : ℕ}
{R : C(↑(Set.Icc 0 T), ℝ)}
(B : Budget period hq D N R)
(hN : N + 6 ≤ q + 1 + 1)
(t : ↑(Set.Icc 0 T))
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1)))
:
EulerSobolevDriftNorm.weightedDriftNorm period 6 N (R t)
(EulerFunctionalVelocity.velocityMap (EulerSobolevTransport.velocityComponents D.κ D.direction))
(D.approximation t + e) ≤ 4 * (B.drift + EulerSobolevGevreyOperators.weightedNorm period 6 N (R t) e)
Only the correction field uses the coarse drift-to-velocity comparison.