Smaller-radius quantitative bounds for the constructed common pressure and the actual first time derivative of the correction.

theorem EulerGevreyCorrectionSourceBounds.sourceBound_scaling (period : ℝ) [Fact (0 < period)] {B0 B1 A0 A2 residual E DE δ : ℝ} (hA2 : 0 ≤ A2) (hE : 0 ≤ E) (hDE : 0 ≤ DE) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (hr : residual ≤ δ) : sourceBound period B0 B1 A0 A2 residual (δ * E) (δ * DE) ≤ sourceBound period B0 B1 A0 A2 1 E DE * δ

Scaling a small error and its first derivatives leaves a linear smallness factor in the actual quadratic source bound.

noncomputable def EulerAllOrderDriftCorrection.Budget.sourceSize (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : ℝ

The explicit raw-source bound before using the target-error smallness.

Equations

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

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

The factor in the correction bound after removing the common delta.

Equations

• EulerAllOrderDriftCorrection.Budget.baseCorrectionSize period B = EulerGevreyMetricEstimate.metricAmplification B.metric.c / 2

noncomputable def EulerAllOrderDriftCorrection.Budget.sourceCost (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : ℝ

An explicit source constant involving only the prescribed norm budgets and the reciprocal initial radius; it is independent of delta.

Equations

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

noncomputable def EulerAllOrderDriftCorrection.Budget.pressureCost (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : ℝ

Pressure cost, given by 2*(B.spatial q hq).full.M*B.sourceCost period q hq.

Equations

• EulerAllOrderDriftCorrection.Budget.pressureCost period B q hq = 2 * (B.spatial q hq).full.M * EulerAllOrderDriftCorrection.Budget.sourceCost period B q hq

noncomputable def EulerAllOrderDriftCorrection.Budget.timeDerivativeCost (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : ℝ

Time derivative cost, given by (1+2*(B.spatial q hq).full.M*(448*(B.spatial q hq).full.B+1))*B.sourceCost period q hq.

Equations

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

theorem EulerAllOrderDriftCorrection.Budget.baseCorrectionSize_nonneg (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : 0 ≤ baseCorrectionSize period B

theorem EulerAllOrderDriftCorrection.Budget.sourceSize_le_delta (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : sourceSize period B q hq ≤ sourceCost period B q hq * B.delta

theorem EulerAllOrderDriftCorrection.Budget.sourceCost_nonneg (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : 0 ≤ sourceCost period B q hq

theorem EulerAllOrderDriftCorrection.Budget.rawSourceTower_reducedNorm (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (N : ℕ) (hNq : N + 4 ≤ q) (s : ℕ) (hs : N + 6 ≤ s) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm period 6 N (reducedRadius period B) (((rawSourceTower period B).realization s) t) ≤ sourceSize period B q hq

The common raw source is bounded at the fixed smaller radius, using only the actual correction and derivative bounds already proved.

theorem EulerAllOrderDriftCorrection.Budget.pressureTower_reducedNorm (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (N : ℕ) (hNq : N + 4 ≤ q) (s : ℕ) (hs : N + 6 ≤ s) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm period 6 N (reducedRadius period B) (((pressureTower period B).realization s) t) ≤ 2 * (B.spatial q hq).full.M * sourceSize period B q hq

The pressure is the actual common signed pressure obtained from the coercive elliptic inverse, with an explicit smaller-radius bound.

theorem EulerAllOrderDriftCorrection.Budget.timeDerivativeTower_reducedNorm (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (N : ℕ) (hNq : N + 4 ≤ q) (s : ℕ) (hs : N + 6 ≤ s) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm period 6 N (reducedRadius period B) (((timeDerivativeTower period B).realization s) t) ≤ (1 + 2 * (B.spatial q hq).full.M * (448 * (B.spatial q hq).full.B + 1)) * sourceSize period B q hq

The actual continuous time-derivative field has the bound obtained from its literal raw-source and signed-pressure equation.

theorem EulerAllOrderDriftCorrection.Budget.pressureTower_reducedNorm_delta (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (N : ℕ) (hNq : N + 4 ≤ q) (s : ℕ) (hs : N + 6 ≤ s) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm period 6 N (reducedRadius period B) (((pressureTower period B).realization s) t) ≤ pressureCost period B q hq * B.delta

The actual pressure-gradient norm is linear in the target error.

theorem EulerAllOrderDriftCorrection.Budget.timeDerivativeTower_reducedNorm_delta (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (N : ℕ) (hNq : N + 4 ≤ q) (s : ℕ) (hs : N + 6 ≤ s) (t : ↑(Set.Icc 0 T)) : EulerSobolevGevreyOperators.weightedNorm period 6 N (reducedRadius period B) (((timeDerivativeTower period B).realization s) t) ≤ timeDerivativeCost period B q hq * B.delta

The actual first time derivative has the same linear target-error factor, at the same fixed radius and every finite external cutoff.