One fixed polynomial controls both correction admissibility and every source multiplier in the same-Q shear/Hessian and graph-flow estimates.

noncomputable def EulerPacketInitializedOutputCost.envelope (W : ℝ) : ℝ

Envelope, constructed using 1.

Equations

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

noncomputable def EulerPacketInitializedOutputCost.polynomial : Polynomial ℝ

Polynomial, constructed using 1.

noncomputable def EulerPacketInitializedOutputCost.uniformConstant : ℝ

Uniform constant, given by coefficientCost polynomial.

Equations

• EulerPacketInitializedOutputCost.uniformConstant = EulerPolynomialCost.coefficientCost EulerPacketInitializedOutputCost.polynomial

noncomputable def EulerPacketInitializedOutputCost.uniformPower : ℕ

Uniform power, given by polynomial.natDegree.

Equations

• EulerPacketInitializedOutputCost.uniformPower = EulerPacketInitializedOutputCost.polynomial.natDegree

theorem EulerPacketInitializedOutputCost.uniformConstant_pos : 0 < uniformConstant

theorem EulerPacketInitializedOutputCost.polynomial_eval (W : ℝ) : Polynomial.eval W polynomial = envelope W

theorem EulerPacketInitializedOutputCost.envelope_bound (W : ℝ) (hW : 1 ≤ W) : envelope W ≤ uniformConstant * W ^ uniformPower

theorem EulerPacketInitializedOutputCost.envelope_components (W : ℝ) (hW : 0 ≤ W) : EulerPacketInitializedCost.uniformConstant * W ^ EulerPacketInitializedCost.uniformPower ≤ envelope W ∧ EulerPacketPhysicalCost.extraEnvelope (EulerPacketInitializedCost.envelope W) ≤ envelope W

theorem EulerPacketInitializedOutputCost.actual_output_costs {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} {hτ : 0 < τ} {hτT : τ < D.T} {B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)} {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (BC : EulerPacketCylinderField.CoefficientBudget C) (δ : ℝ) (ξ : U) (W H0 : ℝ) (hδ : 0 < δ) (H : EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB BC δ ξ W) (hH0 : 0 ≤ H0) (hHW : H0 ≤ W) : have R := EulerPacketTerminalDatum.initializedRadius LM L NB BC δ ξ; have Kc := L.correctionCoefficients NB EulerPacketTerminalDatum.period; have ρ := EulerPacketCorrectionScalar.initialRadius R Kc.M Kc.Rc / 4; have Z := EulerPacketInitializedCost.envelope W; EulerPacketInitializedCost.weightSize W ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerAllOrderDriftCorrection.physicalInputRadius (4 * R) (4 * R) ρ ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerAllOrderDriftCorrection.liftedInputConstant EulerPacketTerminalDatum.period * (EulerPacketCorrectionConstants.velocity R H0 BC.multiplierCost + EulerPacketCorrectionConstants.normal R H0 BC.multiplierCost) ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ 2 * EulerAllOrderDriftCorrection.liftedInputConstant EulerPacketTerminalDatum.period * EulerPacketInitializedCost.weightSize W ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ 2 * EulerAllOrderDriftCorrection.liftedInputConstant EulerPacketTerminalDatum.period * (6 * NB.blockAmplitude * (EulerPacketCylinderField.fixedVelocityGradeCost R H0 1 + EulerPacketCylinderField.fixedVelocityGradeCost R H0 2 + 1) + EulerPacketInitializedCost.weightSize W) ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerAllOrderDriftCorrection.weightedPhysicalGradientCost D EulerPacketTerminalDatum.period L.Rc L.C₀ ρ (EulerPacketInitializedCost.weightSize W) ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerPacketTerminalDatum.initializedGlobalShearCost R H0 NB.C ≤ EulerPacketPhysicalCost.extraEnvelope Z ∧ EulerPacketTerminalDatum.initializedPressureHessianCost NB R H0 L.Rc L.C₀ ≤ EulerPacketPhysicalCost.extraEnvelope Z