Fixed polynomials majorize all primitive coefficient constants of the packet correction. The pressure inverse is the genuine fixed-order recursion.

def EulerPacketCorrectionPrimitive.metricEnvelope (X : ℝ) : ℝ

Metric envelope, given by correctionMetricEnvelope X X.

Equations

• EulerPacketCorrectionPrimitive.metricEnvelope X = EulerPacketCorrectionCoefficients.correctionMetricEnvelope X X

def EulerPacketCorrectionPrimitive.linearEnvelope (X : ℝ) : ℝ

Linear envelope, given by correctionLinearEnvelope X X X.

Equations

• EulerPacketCorrectionPrimitive.linearEnvelope X = EulerPacketCorrectionCoefficients.correctionLinearEnvelope X X X

def EulerPacketCorrectionPrimitive.quadraticEnvelope (X : ℝ) : ℝ

Quadratic envelope, given by correctionQuadraticEnvelope X X X.

Equations

• EulerPacketCorrectionPrimitive.quadraticEnvelope X = EulerPacketCorrectionCoefficients.correctionQuadraticEnvelope X X X

def EulerPacketCorrectionPrimitive.radiusEnvelope (X : ℝ) : ℝ

Radius envelope, given by 1+(1+metricEnvelope X)*(64*X)+64*X.

Equations

• EulerPacketCorrectionPrimitive.radiusEnvelope X = 1 + (1 + EulerPacketCorrectionPrimitive.metricEnvelope X) * (64 * X) + 64 * X

noncomputable def EulerPacketCorrectionPrimitive.pressureEnvelope (X : ℝ) : ℝ

Pressure envelope, given by 1+pressureCost ((1+X)^2)⁻¹ (metricEnvelope X) 5 + pressureCost ((1+X)^2)⁻¹ (metricEnvelope X) 6.

Equations

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

def EulerPacketCorrectionPrimitive.multiplierEnvelope (X : ℝ) : ℝ

Multiplier envelope, given by 3*sobolevCoefficientAmplitude (Fin 4) 6 X X.

Equations

• EulerPacketCorrectionPrimitive.multiplierEnvelope X = 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 X X

noncomputable def EulerPacketCorrectionPrimitive.termEnvelope (P : ℝ) [Fact (0 < P)] (X : ℝ) : ℝ

Term envelope, given by 2*(1+multiplierEnvelope X+9*productBlockConstant P*multiplierEnvelope X).

Equations

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

noncomputable def EulerPacketCorrectionPrimitive.primitiveEnvelope (P : ℝ) [Fact (0 < P)] (X : ℝ) : ℝ

Primitive envelope as an element of ℝ.

Equations

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

noncomputable def EulerPacketCorrectionPrimitive.metricPolynomial : Polynomial ℝ

Metric polynomial, given by coefficientPolynomial 6 (4*Polynomial.X) (3*Polynomial.X*Polynomial.X).

Equations

• EulerPacketCorrectionPrimitive.metricPolynomial = EulerParameterWordGevrey.coefficientPolynomial 6 (4 * Polynomial.X) (3 * Polynomial.X * Polynomial.X)

noncomputable def EulerPacketCorrectionPrimitive.linearPolynomial : Polynomial ℝ

Linear polynomial, given by 2*coefficientPolynomial 6 (4*Polynomial.X) (6*Polynomial.X*Polynomial.X).

Equations

• EulerPacketCorrectionPrimitive.linearPolynomial = 2 * EulerParameterWordGevrey.coefficientPolynomial 6 (4 * Polynomial.X) (6 * Polynomial.X * Polynomial.X)

noncomputable def EulerPacketCorrectionPrimitive.quadraticPolynomial : Polynomial ℝ

Quadratic polynomial, given by 6*coefficientPolynomial 6 (4*Polynomial.X) (3*Polynomial.X*(Polynomial.X*Polynomial.X)).

Equations

• EulerPacketCorrectionPrimitive.quadraticPolynomial = 6 * EulerParameterWordGevrey.coefficientPolynomial 6 (4 * Polynomial.X) (3 * Polynomial.X * (Polynomial.X * Polynomial.X))

noncomputable def EulerPacketCorrectionPrimitive.radiusPolynomial : Polynomial ℝ

Radius polynomial, given by 1+(1+metricPolynomial)*(64*Polynomial.X)+64*Polynomial.X.

Equations

• EulerPacketCorrectionPrimitive.radiusPolynomial = 1 + (1 + EulerPacketCorrectionPrimitive.metricPolynomial) * (64 * Polynomial.X) + 64 * Polynomial.X

noncomputable def EulerPacketCorrectionPrimitive.pressurePolynomialEnvelope : Polynomial ℝ

Pressure polynomial envelope, given by 1+pressurePolynomial ((1+Polynomial.X)^2) metricPolynomial 5 + pressurePolynomial ((1+Polynomial.X)^2) metricPolynomial 6.

Equations

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

noncomputable def EulerPacketCorrectionPrimitive.multiplierPolynomial : Polynomial ℝ

Multiplier polynomial, given by 3*coefficientPolynomial 6 Polynomial.X Polynomial.X.

Equations

• EulerPacketCorrectionPrimitive.multiplierPolynomial = 3 * EulerParameterWordGevrey.coefficientPolynomial 6 Polynomial.X Polynomial.X

noncomputable def EulerPacketCorrectionPrimitive.termPolynomial (P : ℝ) [Fact (0 < P)] : Polynomial ℝ

Term polynomial, given by 2*(1+multiplierPolynomial+9*Polynomial.C (productBlockConstant P)*multiplierPolynomial).

Equations

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

noncomputable def EulerPacketCorrectionPrimitive.primitivePolynomial (P : ℝ) [Fact (0 < P)] : Polynomial ℝ

Primitive polynomial as an element of Polynomial ℝ.

Equations

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

theorem EulerPacketCorrectionPrimitive.metricPolynomial_eval (X : ℝ) : Polynomial.eval X metricPolynomial = metricEnvelope X

theorem EulerPacketCorrectionPrimitive.linearPolynomial_eval (X : ℝ) : Polynomial.eval X linearPolynomial = linearEnvelope X

theorem EulerPacketCorrectionPrimitive.quadraticPolynomial_eval (X : ℝ) : Polynomial.eval X quadraticPolynomial = quadraticEnvelope X

theorem EulerPacketCorrectionPrimitive.radiusPolynomial_eval (X : ℝ) : Polynomial.eval X radiusPolynomial = radiusEnvelope X

theorem EulerPacketCorrectionPrimitive.pressurePolynomialEnvelope_eval (X : ℝ) : Polynomial.eval X pressurePolynomialEnvelope = pressureEnvelope X

theorem EulerPacketCorrectionPrimitive.multiplierPolynomial_eval (X : ℝ) : Polynomial.eval X multiplierPolynomial = multiplierEnvelope X

theorem EulerPacketCorrectionPrimitive.termPolynomial_eval (P : ℝ) [Fact (0 < P)] (X : ℝ) : Polynomial.eval X (termPolynomial P) = termEnvelope P X

theorem EulerPacketCorrectionPrimitive.primitivePolynomial_eval (P : ℝ) [Fact (0 < P)] (X : ℝ) : Polynomial.eval X (primitivePolynomial P) = primitiveEnvelope P X

noncomputable def EulerPacketCorrectionPrimitive.primitiveConstant (P : ℝ) [Fact (0 < P)] : ℝ

Primitive constant, given by coefficientCost (primitivePolynomial P).

Equations

• EulerPacketCorrectionPrimitive.primitiveConstant P = EulerPolynomialCost.coefficientCost (EulerPacketCorrectionPrimitive.primitivePolynomial P)

noncomputable def EulerPacketCorrectionPrimitive.primitivePower (P : ℝ) [Fact (0 < P)] : ℕ

Primitive power, given by (primitivePolynomial P).natDegree.

Equations

• EulerPacketCorrectionPrimitive.primitivePower P = (EulerPacketCorrectionPrimitive.primitivePolynomial P).natDegree

theorem EulerPacketCorrectionPrimitive.primitiveConstant_pos (P : ℝ) [Fact (0 < P)] : 0 < primitiveConstant P

theorem EulerPacketCorrectionPrimitive.primitiveEnvelope_power (P : ℝ) [Fact (0 < P)] (X : ℝ) (hX : 1 ≤ X) : primitiveEnvelope P X ≤ primitiveConstant P * X ^ primitivePower P

theorem EulerPacketCorrectionPrimitive.primitive_components (P X : ℝ) [Fact (0 < P)] (hX : 0 ≤ X) : 1 ≤ primitiveEnvelope P X ∧ 1 + X ≤ primitiveEnvelope P X ∧ X ^ 2 ≤ primitiveEnvelope P X ∧ 3 * X * X * X ≤ primitiveEnvelope P X ∧ 2 * X * X ≤ primitiveEnvelope P X ∧ metricEnvelope X ≤ primitiveEnvelope P X ∧ linearEnvelope X ≤ primitiveEnvelope P X ∧ quadraticEnvelope X ≤ primitiveEnvelope P X ∧ radiusEnvelope X ≤ primitiveEnvelope P X ∧ pressureEnvelope X ≤ primitiveEnvelope P X ∧ multiplierEnvelope X ≤ primitiveEnvelope P X ∧ termEnvelope P X ≤ primitiveEnvelope P X