Actual raw-source, elliptic-pressure, and time-source bounds at a smaller radius.

noncomputable def EulerGevreyCorrectionSourceBounds.sourceBound (period : ℝ) [Fact (0 < period)] (B0 B1 A0 A2 residual E DE : ℝ) : ℝ

The explicit polynomial controlling the literal unprojected correction source.

Equations

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

theorem EulerGevreyCorrectionSourceBounds.sourceBound_nonneg (period : ℝ) [Fact (0 < period)] {B0 B1 A0 A2 residual E DE : ℝ} (hB0 : 0 ≤ B0) (hB1 : 0 ≤ B1) (hA0 : 0 ≤ A0) (hA2 : 0 ≤ A2) (hr : 0 ≤ residual) (hE : 0 ≤ E) (hDE : 0 ≤ DE) : 0 ≤ sourceBound period B0 B1 A0 A2 residual E DE

theorem EulerGevreyCorrectionSourceBounds.weightedNorm_transport (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (r : ℝ) (hr : 0 < r) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerSobolevGevreyOperators.weightedNorm period 6 N r (((EulerSobolevTransport.transportBilinear period hs L hL) u) v) ≤ EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 N r u * ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N r ((EulerCylinderSobolevSpace.derivativeOperator period s i) v)

The actual transport estimate uses the sum of genuine derivative norms, rather than a derivative bound on a hypothetical solution.

theorem EulerGevreyCorrectionSourceBounds.rawSource_smallerRadius_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {P : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D P R) (N : ℕ) (hNP : N ≤ P) (hN : N + 6 ≤ q + 1) (t : ↑(Set.Icc 0 T)) (r : ℝ) (hr : 0 < r) (hrR : r ≤ R t) (E DE : ℝ) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) (he : EulerSobolevGevreyOperators.weightedNorm period 6 N r e ≤ E) (hde : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N r ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) e) ≤ DE) : EulerSobolevGevreyOperators.weightedNorm period 6 N r (EulerCorrectionOperators.CorrectionData.rawSource period D hq t e) ≤ sourceBound period S.B0 S.B1 S.A0 S.A2 S.residual E DE

All inputs on the right are the actual prescribed coefficient and background budgets, and norms of the given error and its derivatives.

theorem EulerGevreyCorrectionSourceBounds.pressure_smallerRadius_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {P : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D P R) (N : ℕ) (hNP : N ≤ P) (hN : N + 6 ≤ q + 1) (t : ↑(Set.Icc 0 T)) (r : ℝ) (hr : 0 < r) (hrR : r ≤ R t) (E DE : ℝ) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) (he : EulerSobolevGevreyOperators.weightedNorm period 6 N r e ≤ E) (hde : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N r ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) e) ≤ DE) : EulerSobolevGevreyOperators.weightedNorm period 6 N r (EulerCorrectionOperators.CorrectionData.pressure period D hq t e) ≤ 2 * S.M * sourceBound period S.B0 S.B1 S.A0 S.A2 S.residual E DE

The actual elliptic inverse acts at the smaller radius using the same proved coefficient budget.

theorem EulerGevreyCorrectionSourceBounds.metric_smallerRadius_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {P : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D P R) (N : ℕ) (hNP : N ≤ P) (t : ↑(Set.Icc 0 T)) (r : ℝ) (hr : 0 < r) (hrR : r ≤ R t) : EulerSobolevGevreyOperators.weightedCoefficient period (D.metric.jet t) 6 N r ≤ 448 * S.B + 1

The metric multiplication cost remains independent of the cutoff.

theorem EulerGevreyCorrectionSourceBounds.timeSource_smallerRadius_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {P : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D P R) (N : ℕ) (hNP : N ≤ P) (hN : N + 6 ≤ q + 1) (t : ↑(Set.Icc 0 T)) (r : ℝ) (hr : 0 < r) (hrR : r ≤ R t) (E DE : ℝ) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) (he : EulerSobolevGevreyOperators.weightedNorm period 6 N r e ≤ E) (hde : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N r ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) e) ≤ DE) : EulerSobolevGevreyOperators.weightedNorm period 6 N r ((EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply t e) ≤ (1 + 2 * S.M * (448 * S.B + 1)) * sourceBound period S.B0 S.B1 S.A0 S.A2 S.residual E DE

The actual projected time source is bounded by the raw source and its constructed signed pressure, with no time-derivative hypothesis.