A single explicit polynomial controls the five scalar costs used by the actual all-order packet correction. This is a uniform estimate on primitive source bounds, not a per-parent eventual-frequency assertion.

@[instance_reducible]

noncomputable def EulerPacketFiveCost.instPacketFiveCostPolynomial1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketFiveCost.instPacketFiveCostPolynomial1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketFiveCost.instPacketFiveCostPolynomial2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketFiveCost.instPacketFiveCostPolynomial2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketFiveCost.instPacketFiveCostPolynomial3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ (Space →L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerPacketFiveCost.instPacketFiveCostPolynomial3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketFiveCost.instPacketFiveCostPolynomial4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ (Space →L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerPacketFiveCost.instPacketFiveCostPolynomial4 = inferInstance

noncomputable def EulerPacketFiveCost.rawGrowth (P : ℝ) [Fact (0 < P)] (i m f t B M A0 A2 B0 B1 : ℝ) : ℝ

The growth constant written in inverse-coercivity variables.

Equations

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

noncomputable def EulerPacketFiveCost.growthEnvelope (P : ℝ) [Fact (0 < P)] (X : ℝ) : ℝ

Growth envelope, given by rawGrowth P X X X X X X X X (2*velocity X X X) (48*velocity X X X*X).

Equations

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

def EulerPacketFiveCost.inverseRadiusEnvelope (X : ℝ) : ℝ

Inverse radius envelope, given by 1+8*X+4*X^2+X.

Equations

• EulerPacketFiveCost.inverseRadiusEnvelope X = 1 + 8 * X + 4 * X ^ 2 + X

noncomputable def EulerPacketFiveCost.fiveEnvelope (P : ℝ) [Fact (0 < P)] (X : ℝ) : ℝ

Five envelope as an element of ℝ.

Equations

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

noncomputable def EulerPacketFiveCost.gradePolynomial (n : ℕ) : Polynomial ℝ

Grade polynomial, given by 3*Polynomial.X^(2*n)*((4*Polynomial.X)^(highShift n) * Polynomial.C ((highShift n).factorial : ℝ)^2).

noncomputable def EulerPacketFiveCost.velocityPolynomial : Polynomial ℝ

Velocity polynomial, given by Polynomial.X*(gradePolynomial 1+gradePolynomial 2+1).

noncomputable def EulerPacketFiveCost.driftPolynomial : Polynomial ℝ

Drift polynomial, given by 2*(3*velocityPolynomial+Polynomial.X*(gradePolynomial 2+2)).

noncomputable def EulerPacketFiveCost.growthPolynomial (P : ℝ) [Fact (0 < P)] : Polynomial ℝ

Growth polynomial as an element of Polynomial ℝ.

noncomputable def EulerPacketFiveCost.fivePolynomial (P : ℝ) [Fact (0 < P)] : Polynomial ℝ

Five polynomial as an element of Polynomial ℝ.

theorem EulerPacketFiveCost.gradePolynomial_eval (n : ℕ) (X : ℝ) : Polynomial.eval X (gradePolynomial n) = EulerPacketCylinderField.fixedVelocityGradeCost X X n

theorem EulerPacketFiveCost.velocityPolynomial_eval (X : ℝ) : Polynomial.eval X velocityPolynomial = EulerPacketCorrectionConstants.velocity X X X

theorem EulerPacketFiveCost.driftPolynomial_eval (X : ℝ) : Polynomial.eval X driftPolynomial = EulerPacketCorrectionConstants.drift X X X

theorem EulerPacketFiveCost.growthPolynomial_eval (P : ℝ) [Fact (0 < P)] (X : ℝ) : Polynomial.eval X (growthPolynomial P) = growthEnvelope P X

theorem EulerPacketFiveCost.fivePolynomial_eval (P : ℝ) [Fact (0 < P)] (X : ℝ) : Polynomial.eval X (fivePolynomial P) = fiveEnvelope P X

noncomputable def EulerPacketFiveCost.costConstant (P : ℝ) [Fact (0 < P)] : ℝ

Cost constant, given by coefficientCost (fivePolynomial P).

Equations

• EulerPacketFiveCost.costConstant P = EulerPolynomialCost.coefficientCost (EulerPacketFiveCost.fivePolynomial P)

noncomputable def EulerPacketFiveCost.costPower (P : ℝ) [Fact (0 < P)] : ℕ

Cost power, given by (fivePolynomial P).natDegree.

Equations

• EulerPacketFiveCost.costPower P = (EulerPacketFiveCost.fivePolynomial P).natDegree

theorem EulerPacketFiveCost.costConstant_pos (P : ℝ) [Fact (0 < P)] : 0 < costConstant P

theorem EulerPacketFiveCost.fiveEnvelope_power (P : ℝ) [Fact (0 < P)] (X : ℝ) (hX : 1 ≤ X) : fiveEnvelope P X ≤ costConstant P * X ^ costPower P

theorem EulerPacketFiveCost.velocity_mono {R H C X : ℝ} (hR : 0 ≤ R) (hH : 0 ≤ H) (_hC : 0 ≤ C) (hRX : R ≤ X) (hHX : H ≤ X) (hCX : C ≤ X) : EulerPacketCorrectionConstants.velocity R H C ≤ EulerPacketCorrectionConstants.velocity X X X

theorem EulerPacketFiveCost.drift_mono {R H C X : ℝ} (hR : 0 ≤ R) (hH : 0 ≤ H) (hC : 0 ≤ C) (hRX : R ≤ X) (hHX : H ≤ X) (hCX : C ≤ X) : EulerPacketCorrectionConstants.drift R H C ≤ EulerPacketCorrectionConstants.drift X X X

@[instance_reducible]

noncomputable def EulerPacketFiveCost.instPacketFiveCostPolynomial5 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) : NormedAddCommGroup C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup C(Set.Icc (0 : ℝ) D.T, Space →ᵇ (Space →L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerPacketFiveCost.instPacketFiveCostPolynomial5 D = inferInstance

theorem EulerPacketFiveCost.growth_eq_raw (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P) (R H C : ℝ) : EulerPacketCorrectionConstants.growth D P Kc R H C = rawGrowth P D.inverseBound (EulerPacketCorrectionCoefficients.inverseMetricBound D) (EulerPacketCorrectionCoefficients.inverseMetricFirstBound D) (EulerPacketCorrectionCoefficients.inverseMetricTimeBound D) Kc.B Kc.M Kc.A0 Kc.A2 (2 * EulerPacketCorrectionConstants.velocity R H C) (48 * EulerPacketCorrectionConstants.velocity R H C * R)

theorem EulerPacketFiveCost.growth_le_envelope (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) (hm : EulerPacketCorrectionCoefficients.inverseMetricBound D ≤ X) (hf : EulerPacketCorrectionCoefficients.inverseMetricFirstBound D ≤ X) (ht : EulerPacketCorrectionCoefficients.inverseMetricTimeBound D ≤ X) (hB : Kc.B ≤ X) (hM : Kc.M ≤ X) (hA0 : Kc.A0 ≤ X) (hA2 : Kc.A2 ≤ X) : EulerPacketCorrectionConstants.growth D P Kc R H C ≤ growthEnvelope P X