Actual weighted correction and derivative bounds at a fixed positive radius.
noncomputable def
EulerAllOrderDriftCorrection.Budget.reducedRadius
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
:
The fixed radius retained for the correction, its pressure, and its time derivative.
Equations
- EulerAllOrderDriftCorrection.Budget.reducedRadius period B = B.initialRadius / 4
Instances For
noncomputable def
EulerAllOrderDriftCorrection.Budget.correctionSize
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
:
The actual target-error envelope converted from metric energy to the fixed H⁶ word norm.
Equations
Instances For
theorem
EulerAllOrderDriftCorrection.Budget.growth_pos
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
:
theorem
EulerAllOrderDriftCorrection.Budget.radius_bounds
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerAllOrderDriftCorrection.Budget.reducedRadius_pos
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
:
theorem
EulerAllOrderDriftCorrection.Budget.reducedRadius_le_half
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerAllOrderDriftCorrection.Budget.correctionSize_nonneg
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
:
theorem
EulerAllOrderDriftCorrection.Budget.fieldTower_weightedNorm_residual
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(q : ℕ)
(hq : 6 ≤ q)
(N : ℕ)
(hN : N ≤ q - 4)
(hNq : N + 6 ≤ q + 1)
(s : ℕ)
(hs : N + 6 ≤ s)
(t : ↑(Set.Icc 0 T))
:
EulerSobolevGevreyOperators.weightedNorm period 6 N (B.radius t) (((fieldTower period B).realization s) t) ≤ EulerGevreyMetricEstimate.metricAmplification B.metric.c * (2 * (B.spatial q hq).full.residual * Real.exp (3 * B.growthCoefficient * ↑t))
The actual common correction retains the quantitative residual energy of any finite realization containing the requested words.
theorem
EulerAllOrderDriftCorrection.Budget.fieldTower_weightedNorm_delta
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(s N : ℕ)
(hN : N + 6 ≤ s)
(t : ↑(Set.Icc 0 T))
:
EulerSobolevGevreyOperators.weightedNorm period 6 N (B.radius t) (((fieldTower period B).realization s) t) ≤ correctionSize period B
At every finite cutoff, the norm bounds the one constructed common field.
theorem
EulerAllOrderDriftCorrection.Budget.fieldTower_reducedNorm
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(s N : ℕ)
(hN : N + 6 ≤ s)
(t : ↑(Set.Icc 0 T))
:
EulerSobolevGevreyOperators.weightedNorm period 6 N (reducedRadius period B) (((fieldTower period B).realization s) t) ≤ correctionSize period B
The correction estimate holds at the same fixed quarter of the initial radius for the whole time interval.
theorem
EulerAllOrderDriftCorrection.Budget.fieldTower_reducedDerivativeNorm
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(s N : ℕ)
(hN : N + 6 ≤ s)
(t : ↑(Set.Icc 0 T))
:
∑ i : Fin 4,
EulerSobolevGevreyOperators.weightedNorm period 6 N (reducedRadius period B)
((EulerCylinderSobolevSpace.derivativeOperator period s i) (((fieldTower period B).realization (s + 1)) t)) ≤ 8 / B.initialRadius * correctionSize period B
One extra derivative costs only the fixed reciprocal initial radius. The estimate is simultaneous in all four genuine coordinate derivatives.
theorem
EulerAllOrderDriftCorrection.Budget.residual_le_delta
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(q : ℕ)
(hq : 6 ≤ q)
:
The scalar residual budget itself is small; this follows from the actual bootstrap input and does not assume a pressure estimate.