Uniform polynomial bounds for the actual correction, pressure and time-derivative amplitudes at the retained radius.

Fixed source constants in the smaller-radius estimates for the actual initialized all-order correction. They do not depend on the cutoff or frequency.

noncomputable def EulerPacketCorrectionConstants.correctionBase {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : ℝ

Correction base, given by metricAmplification D.inverseBound⁻¹/2.

Equations

• EulerPacketCorrectionConstants.correctionBase D = EulerGevreyMetricEstimate.metricAmplification D.inverseBound⁻¹ / 2

noncomputable def EulerPacketCorrectionConstants.correctionSourceCost {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P) (R H C : ℝ) : ℝ

Correction source cost, constructed using sourceBound.

Equations

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

noncomputable def EulerPacketCorrectionConstants.correctionPressureCost {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P) (R H C : ℝ) : ℝ

Correction pressure cost, given by 2*Kc.M*correctionSourceCost D P Kc R H C.

Equations

• EulerPacketCorrectionConstants.correctionPressureCost D P Kc R H C = 2 * Kc.M * EulerPacketCorrectionConstants.correctionSourceCost D P Kc R H C

noncomputable def EulerPacketCorrectionConstants.correctionTimeCost {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P) (R H C : ℝ) : ℝ

Correction time cost, given by (1+2*Kc.M*(448*Kc.B+1))*correctionSourceCost D P Kc R H C.

Equations

• EulerPacketCorrectionConstants.correctionTimeCost D P Kc R H C = (1 + 2 * Kc.M * (448 * Kc.B + 1)) * EulerPacketCorrectionConstants.correctionSourceCost D P Kc R H C

noncomputable def EulerPacketCorrectionOutput.baseEnvelope (X : ℝ) : ℝ

Base envelope, given by (1+Real.sqrt 5461*X)/2.

Equations

• EulerPacketCorrectionOutput.baseEnvelope X = (1 + √5461 * X) / 2

noncomputable def EulerPacketCorrectionOutput.sourceEnvelope (P : ℝ) [Fact (0 < P)] (X : ℝ) : ℝ

Source envelope, given by sourceBound P (2*velocity X X X) (48*velocity X X X*X) X X 1 (baseEnvelope X) (8*inverseRadiusEnvelope X*baseEnvelope X).

Equations

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

noncomputable def EulerPacketCorrectionOutput.outputEnvelope (P : ℝ) [Fact (0 < P)] (X : ℝ) : ℝ

Output envelope, given by 1+baseEnvelope X+2*X*sourceEnvelope P X+(1+2*X*(448*X+1))*sourceEnvelope P X.

Equations

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

noncomputable def EulerPacketCorrectionOutput.outputPolynomial (P : ℝ) [Fact (0 < P)] : Polynomial ℝ

Output polynomial as an element of Polynomial ℝ.

theorem EulerPacketCorrectionOutput.outputPolynomial_eval (P : ℝ) [Fact (0 < P)] (X : ℝ) : Polynomial.eval X (outputPolynomial P) = outputEnvelope P X

noncomputable def EulerPacketCorrectionOutput.outputConstant (P : ℝ) [Fact (0 < P)] : ℝ

Output constant, given by coefficientCost (outputPolynomial P).

Equations

• EulerPacketCorrectionOutput.outputConstant P = EulerPolynomialCost.coefficientCost (EulerPacketCorrectionOutput.outputPolynomial P)

noncomputable def EulerPacketCorrectionOutput.outputPower (P : ℝ) [Fact (0 < P)] : ℕ

Output power, given by (outputPolynomial P).natDegree.

Equations

• EulerPacketCorrectionOutput.outputPower P = (EulerPacketCorrectionOutput.outputPolynomial P).natDegree

theorem EulerPacketCorrectionOutput.outputConstant_pos (P : ℝ) [Fact (0 < P)] : 0 < outputConstant P

theorem EulerPacketCorrectionOutput.outputEnvelope_power (P : ℝ) [Fact (0 < P)] (X : ℝ) (hX : 1 ≤ X) : outputEnvelope P X ≤ outputConstant P * X ^ outputPower P

theorem EulerPacketCorrectionOutput.output_components (P : ℝ) [Fact (0 < P)] (X : ℝ) (hX : 0 ≤ X) : 1 ≤ outputEnvelope P X ∧ baseEnvelope X ≤ outputEnvelope P X ∧ 2 * X * sourceEnvelope P X ≤ outputEnvelope P X ∧ (1 + 2 * X * (448 * X + 1)) * sourceEnvelope P X ≤ outputEnvelope P X

theorem EulerPacketCorrectionOutput.correctionBase_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : 0 ≤ EulerPacketCorrectionConstants.correctionBase D

theorem EulerPacketCorrectionOutput.correctionSourceCost_nonneg (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P) (R H C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) : 0 ≤ EulerPacketCorrectionConstants.correctionSourceCost D P Kc R H C

theorem EulerPacketCorrectionOutput.correction_output_bound (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P) (R H C X : ℝ) (hR : 0 ≤ R) (hH : 0 ≤ H) (hC : 0 ≤ C) (hRX : R ≤ X) (hHX : H ≤ X) (hCX : C ≤ X) (hi : D.inverseBound ≤ X) (hB : Kc.B ≤ X) (hM : Kc.M ≤ X) (hA0 : Kc.A0 ≤ X) (hA2 : Kc.A2 ≤ X) (hRc : Kc.Rc ≤ X) : 0 ≤ EulerPacketCorrectionConstants.correctionBase D ∧ 0 ≤ EulerPacketCorrectionConstants.correctionPressureCost D P Kc R H C ∧ 0 ≤ EulerPacketCorrectionConstants.correctionTimeCost D P Kc R H C ∧ EulerPacketCorrectionConstants.correctionBase D ≤ outputEnvelope P X ∧ EulerPacketCorrectionConstants.correctionPressureCost D P Kc R H C ≤ outputEnvelope P X ∧ EulerPacketCorrectionConstants.correctionTimeCost D P Kc R H C ≤ outputEnvelope P X