Polynomial control of the original source-solver radii, before the canonical primary/common enlargement. The boundary coefficient L is an explicit primitive input.

def EulerPacketSourceRadius.forcingEnvelope (W : ℝ) : ℝ

Forcing envelope, given by 3*coeff W (2*W).

Equations

• EulerPacketSourceRadius.forcingEnvelope W = 3 * EulerPacketRadiusPolynomial.coeff W (2 * W)

def EulerPacketSourceRadius.accelerationEnvelope (W : ℝ) : ℝ

Acceleration envelope, given by 3*coeff W W*(1+6*coeff W W*(W+2)).

Equations

• EulerPacketSourceRadius.accelerationEnvelope W = 3 * EulerPacketRadiusPolynomial.coeff W W * (1 + 6 * EulerPacketRadiusPolynomial.coeff W W * (W + 2))

noncomputable def EulerPacketSourceRadius.operatorEnvelope (W : ℝ) : ℝ

Operator envelope, given by 36*W^2*(1+2*W+W*scaledBoundaryOperatorAmplitude).

Equations

• EulerPacketSourceRadius.operatorEnvelope W = 36 * W ^ 2 * (1 + 2 * W + W * EulerMeanBoundary.scaledBoundaryOperatorAmplitude)

def EulerPacketSourceRadius.projectedEnvelope (W : ℝ) : ℝ

Projected envelope, given by 3*coeff (4*W) (3*W^2).

Equations

• EulerPacketSourceRadius.projectedEnvelope W = 3 * EulerPacketRadiusPolynomial.coeff (4 * W) (3 * W ^ 2)

noncomputable def EulerPacketSourceRadius.primitiveLift (W : ℝ) : ℝ

Primitive lift, given by 1+(W+2)+formEnvelope W+forcingEnvelope W+3*W^2+accelerationEnvelope W + operatorEnvelope W+projectedEnvelope W.

Equations

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

noncomputable def EulerPacketSourceRadius.sourceRadiusEnvelope (W : ℝ) : ℝ

Source radius envelope, given by let V := primitiveLift W 1+V+6*weakEnvelope V*(16*V+1)+64*V+2*forwardEnvelope V*(64*V+1).

Equations

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

theorem EulerPacketSourceRadius.primitiveLift_bounds (W : ℝ) (hW : 0 ≤ W) : 1 ≤ primitiveLift W ∧ W + 2 ≤ primitiveLift W ∧ EulerPacketRadiusPolynomial.formEnvelope W ≤ primitiveLift W ∧ forcingEnvelope W ≤ primitiveLift W ∧ 3 * W ^ 2 ≤ primitiveLift W ∧ accelerationEnvelope W ≤ primitiveLift W ∧ operatorEnvelope W ≤ primitiveLift W ∧ projectedEnvelope W ≤ primitiveLift W

theorem EulerPacketSourceRadius.coeff_self_lower (W : ℝ) (hW : 0 ≤ W) : W ≤ EulerPacketRadiusPolynomial.coeff W W

theorem EulerPacketSourceRadius.weakEnvelope_lower_inputs (V : ℝ) (hV : 1 ≤ V) : V ≤ EulerPacketRadiusPolynomial.inverseEnvelope V ∧ V ≤ EulerPacketRadiusPolynomial.formEnvelope V ∧ V ≤ 3 * EulerPacketRadiusPolynomial.coeff V (2 * V) * EulerPacketRadiusPolynomial.endpointEnvelope V

theorem EulerPacketSourceRadius.block_le_weak (V : ℝ) (hV : 1 ≤ V) (I R C D : ℝ) (hI0 : 0 ≤ I) (hR0 : 0 ≤ R) (hC0 : 0 ≤ C) (hD0 : 0 ≤ D) (hI : I ≤ V) (hR : R ≤ V) (hC : C ≤ V) (hD : D ≤ V) : EulerParameterWordGevrey.inverseBlockCost (Fin 4) 6 I R C D ≤ EulerPacketRadiusPolynomial.weakEnvelope V

theorem EulerPacketSourceRadius.form_scalar_le (T C C1 H W : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (hC : 0 ≤ C) (hC1 : 0 ≤ C1) (hH : 0 ≤ H) (hCW : C ≤ W) (hC1W : C1 ≤ W) (hHW : H ≤ W) : 9 * (T * C1 + C) ^ 2 * (1 + T ^ 2 * H) ≤ EulerPacketRadiusPolynomial.formEnvelope W

theorem EulerPacketSourceRadius.forcing_scalar_le (T R C C1 W : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC1 : 0 ≤ C1) (hRW : R ≤ W) (hCW : C ≤ W) (hC1W : C1 ≤ W) : 3 * EulerPacketRadiusPolynomial.coeff R (T * (T * C1 + C)) ≤ forcingEnvelope W

theorem EulerPacketSourceRadius.acceleration_scalar_le (R C C1 Cv W : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC1 : 0 ≤ C1) (hCv : 0 ≤ Cv) (hW : 0 ≤ W) (hRW : R ≤ W) (hCW : C ≤ W) (hC1W : C1 ≤ W) (hCvW : Cv ≤ W + 2) : EulerParameterWordGevrey.accelerationBlockAmplitude (Fin 4) 6 R C C1 1 Cv ≤ accelerationEnvelope W

theorem EulerPacketSourceRadius.operator_scalar_le (T C C1 H L W : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (hC : 0 ≤ C) (hC1 : 0 ≤ C1) (hH : 0 ≤ H) (hL : 0 ≤ L) (hCW : C ≤ W) (hC1W : C1 ≤ W) (hHW : H ≤ W) (hLW : L ≤ W) : EulerMeanTranslatedGevrey.operatorAmplitude T C C1 H C1 EulerMeanBoundary.scaledBoundaryOperatorAmplitude L ≤ operatorEnvelope W

theorem EulerPacketSourceRadius.projected_scalar_le (Ri C W : ℝ) (hRi : 0 ≤ Ri) (hC : 0 ≤ C) (hW : 0 ≤ W) (hi : Ri ≤ W) (hc : C ≤ W) : EulerSourceCylinderForwardSobolev.forcingCost (Fin 4) 6 Ri C ≤ projectedEnvelope W

theorem EulerPacketSourceRadius.forward_scalar_le (T C A D CB R V : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (hC : 0 ≤ C) (hA : 0 ≤ A) (hD : 0 ≤ D) (hCB : 0 ≤ CB) (hR : 0 ≤ R) (hV : 0 ≤ V) (hCV : C ≤ V) (hAV : A ≤ V) (hDV : D ≤ V) (hCBV : CB ≤ 18 * V ^ 3) (hRV : R ≤ 4 * V) : EulerLinearDuhamel.forwardSobolevCost (Fin 4) 6 T C A D CB R ≤ EulerPacketRadiusPolynomial.forwardEnvelope V

theorem EulerPacketSourceRadius.joined_radius_le (T S Ti R C C1 C2 Cp W : ℝ) (hW : 1 ≤ W) (hT0 : 0 ≤ T) (hT : T ≤ 1) (hS0 : 0 ≤ S) (hS : S ≤ 1) (hTi0 : 0 ≤ Ti) (hTi : Ti ≤ W) (hR0 : 0 ≤ R) (hR : R ≤ W) (hC0 : 0 ≤ C) (hC : C ≤ W) (hC10 : 0 ≤ C1) (hC1 : C1 ≤ W) (hC20 : 0 ≤ C2) (hCp0 : 0 ≤ Cp) (hCp : Cp ≤ W) (hH : 27 * C ^ 2 * C2 ≤ W) (hI : EulerPacketParentMeanCoercivity.inverseEnvelope C C1 ≤ W) (hGram : EulerPacketParentMeanCoercivity.gramInverseEnvelope C ≤ W) (hRi : EulerPacketParentTransverseCosts.inverseRadius R C ≤ W) : EulerPacketParentTransverseCosts.radius 6 T S Ti R C C1 C2 Cp ≤ sourceRadiusEnvelope W

theorem EulerPacketSourceRadius.mean_radius_le (T Ti R C C1 C2 L W : ℝ) (hW : 1 ≤ W) (hT0 : 0 ≤ T) (hT : T ≤ 1) (hTi0 : 0 ≤ Ti) (hTi : Ti ≤ W) (hR0 : 0 ≤ R) (hR : R ≤ W) (hC0 : 0 ≤ C) (hC : C ≤ W) (hC10 : 0 ≤ C1) (hC1 : C1 ≤ W) (hC20 : 0 ≤ C2) (hL0 : 0 ≤ L) (hL : L ≤ W) (hH : 27 * C ^ 2 * C2 ≤ W) (hI : EulerPacketParentMeanCoercivity.inverseEnvelope C C1 ≤ W) (hGram : EulerPacketParentMeanCoercivity.gramInverseEnvelope C ≤ W) : EulerPacketParentMeanBudget.radius 6 T Ti R C C1 C2 L ≤ sourceRadiusEnvelope W

theorem EulerPacketSourceRadius.le_sourceRadiusEnvelope (W : ℝ) (hW : 0 ≤ W) : W ≤ sourceRadiusEnvelope W

noncomputable def EulerPacketSourceRadius.primitivePolynomial : Polynomial ℝ

Primitive polynomial as an element of Polynomial ℝ.

Equations

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

theorem EulerPacketSourceRadius.primitivePolynomial_eval (W : ℝ) : Polynomial.eval W primitivePolynomial = primitiveLift W

noncomputable def EulerPacketSourceRadius.sourceRadiusPolynomial : Polynomial ℝ

Source radius polynomial as an element of Polynomial ℝ.

Equations

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

theorem EulerPacketSourceRadius.sourceRadiusPolynomial_eval (W : ℝ) : Polynomial.eval W sourceRadiusPolynomial = sourceRadiusEnvelope W

noncomputable def EulerPacketSourceRadius.sourceRadiusConstant : ℝ

Source radius constant, given by coefficientCost sourceRadiusPolynomial.

Equations

• EulerPacketSourceRadius.sourceRadiusConstant = EulerPolynomialCost.coefficientCost EulerPacketSourceRadius.sourceRadiusPolynomial

noncomputable def EulerPacketSourceRadius.sourceRadiusPower : ℕ

Source radius power, given by sourceRadiusPolynomial.natDegree.

Equations

• EulerPacketSourceRadius.sourceRadiusPower = EulerPacketSourceRadius.sourceRadiusPolynomial.natDegree

theorem EulerPacketSourceRadius.sourceRadiusConstant_pos : 0 < sourceRadiusConstant

theorem EulerPacketSourceRadius.sourceRadiusEnvelope_power (W : ℝ) (hW : 1 ≤ W) : sourceRadiusEnvelope W ≤ sourceRadiusConstant * W ^ sourceRadiusPower