Polynomial formulas for the fixed-order inverse and for a common source-radius envelope. No target radius, forcing amplitude or grade occurs in the primitive envelope.

def EulerParameterWordGevrey.inversePolynomial (I B : Polynomial ℝ) : ℕ → Polynomial ℝ

Inverse polynomial as an element of ℕ → Polynomial ℝ | 0 => I | n+1 => I+inversePolynomial I B n+2^n*B*(inversePolynomial I B n)^2.

Equations

• EulerParameterWordGevrey.inversePolynomial I B 0 = I
• EulerParameterWordGevrey.inversePolynomial I B n.succ = I + EulerParameterWordGevrey.inversePolynomial I B n + 2 ^ n * B * EulerParameterWordGevrey.inversePolynomial I B n ^ 2

theorem EulerParameterWordGevrey.inversePolynomial_eval (I B : Polynomial ℝ) (n : ℕ) (x : ℝ) : Polynomial.eval x (inversePolynomial I B n) = sobolevInverseCost (Polynomial.eval x I) (Polynomial.eval x B) n

noncomputable def EulerParameterWordGevrey.inverseBlockPolynomial (q : ℕ) (I R C D : Polynomial ℝ) : Polynomial ℝ

Inverse block polynomial, given by 1+inversePolynomial I (coefficientPolynomial q R C) q*(coefficientPolynomial q R C+D).

Equations

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

theorem EulerParameterWordGevrey.inverseBlockPolynomial_eval (q : ℕ) (I R C D : Polynomial ℝ) (x : ℝ) : Polynomial.eval x (inverseBlockPolynomial q I R C D) = inverseBlockCost (Fin 4) q (Polynomial.eval x I) (Polynomial.eval x R) (Polynomial.eval x C) (Polynomial.eval x D)

theorem EulerParameterWordGevrey.inverseBlockCost_mono_all {ι : Type u_1} [Fintype ι] (q : ℕ) {I R C D I' R' C' D' : ℝ} (hI : 0 ≤ I) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (hi : I ≤ I') (hr : R ≤ R') (hc : C ≤ C') (hd : D ≤ D') : inverseBlockCost ι q I R C D ≤ inverseBlockCost ι q I' R' C' D'

theorem EulerParameterWordGevrey.inverseBlockCost_one_le {ι : Type u_1} [Fintype ι] (q : ℕ) {I R C D : ℝ} (hI : 0 ≤ I) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) : 1 ≤ inverseBlockCost ι q I R C D

@[reducible, inline]

abbrev EulerPacketRadiusPolynomial.coeff (R C : ℝ) : ℝ

Coeff: an abbreviation for sobolevCoefficientAmplitude (Fin 4) 6 R C.

Equations

• EulerPacketRadiusPolynomial.coeff R C = EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 R C

@[reducible, inline]

noncomputable abbrev EulerPacketRadiusPolynomial.coeffPoly (R C : Polynomial ℝ) : Polynomial ℝ

Coeff poly: an abbreviation for coefficientPolynomial 6 R C.

Equations

• EulerPacketRadiusPolynomial.coeffPoly R C = EulerParameterWordGevrey.coefficientPolynomial 6 R C

def EulerPacketRadiusPolynomial.inverseEnvelope (W : ℝ) : ℝ

Inverse envelope, given by 2*(1+2*W^5+2*W^2)^2.

Equations

• EulerPacketRadiusPolynomial.inverseEnvelope W = 2 * (1 + 2 * W ^ 5 + 2 * W ^ 2) ^ 2

def EulerPacketRadiusPolynomial.formEnvelope (W : ℝ) : ℝ

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

Equations

• EulerPacketRadiusPolynomial.formEnvelope W = 36 * W ^ 2 * (1 + W)

def EulerPacketRadiusPolynomial.endpointEnvelope (W : ℝ) : ℝ

Endpoint envelope, given by 6*coeff W W*W.

Equations

• EulerPacketRadiusPolynomial.endpointEnvelope W = 6 * EulerPacketRadiusPolynomial.coeff W W * W

def EulerPacketRadiusPolynomial.weakEnvelope (W : ℝ) : ℝ

Weak envelope, given by inverseBlockCost (Fin 4) 6 (inverseEnvelope W) W (formEnvelope W) (3*coeff W (2*W)*endpointEnvelope W).

Equations

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

def EulerPacketRadiusPolynomial.strongEnvelope (W : ℝ) : ℝ

Strong envelope, given by inverseBlockCost (Fin 4) 6 W W (3*W^2) (3*coeff W W*(endpointEnvelope W+6*coeff W W*(2*W+2))).

Equations

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

def EulerPacketRadiusPolynomial.forwardEnvelope (W : ℝ) : ℝ

Forward envelope, given by let b := coeff (4*W) (1+36*W^4) 1+sobolevInverseCost 1 b 6*(b+W*(2*W+2)).

Equations

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

def EulerPacketRadiusPolynomial.jetEnvelope (W : ℝ) : ℝ

Jet envelope, given by 64+40*W^2.

Equations

• EulerPacketRadiusPolynomial.jetEnvelope W = 64 + 40 * W ^ 2

def EulerPacketRadiusPolynomial.requiredEnvelope (W : ℝ) : ℝ

Required envelope, given by `W+16jetEnvelope W+2(weakEnvelope W+strongEnvelope W)(16W+1)

• 2forwardEnvelope W(64*W+1)`.

Equations

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

def EulerPacketRadiusPolynomial.physicalEnvelope (W : ℝ) : ℝ

Physical envelope, given by let a := coeff (4*W) W 3*a+3*a*(3*coeff (4*W) (18*W^3)+3*coeff (4*W) (3*W^2)).

Equations

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

def EulerPacketRadiusPolynomial.commonEnvelope (W : ℝ) : ℝ

Common envelope, given by 6*coeff W W*(2*W+2)+6*coeff W W+physicalEnvelope W.

Equations

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

def EulerPacketRadiusPolynomial.normalEnvelope (W : ℝ) : ℝ

Normal envelope, given by coeff (5*W+1) (1+W+6*W^2+729*W^6).

Equations

• EulerPacketRadiusPolynomial.normalEnvelope W = EulerPacketRadiusPolynomial.coeff (5 * W + 1) (1 + W + 6 * W ^ 2 + 729 * W ^ 6)

def EulerPacketRadiusPolynomial.pressureEnvelope (W : ℝ) : ℝ

Pressure envelope, given by 3*coeff (4*W) (3*W^2)*(1+6*coeff (4*W) W*commonEnvelope W).

Equations

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

noncomputable def EulerPacketRadiusPolynomial.gradeEnvelope (W : ℝ) : ℝ

Grade envelope, given by commonEnvelope W+135*(normalEnvelope W)^2*(period*commonEnvelope W) + 3*period*pressureEnvelope W.

Equations

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

def EulerPacketRadiusPolynomial.meanEnvelope (W : ℝ) : ℝ

Mean envelope, given by let a := coeff W W 3*a*(W+2)+3*(a*(W+2)+a)+3*a*(W+3*a+6*a*(W+2)).

Equations

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

noncomputable def EulerPacketRadiusPolynomial.terminalEnvelope (W : ℝ) : ℝ

Terminal envelope, given by coeff (jetEnvelope W) (300*(9/rawBump 0)^3*W^2*terminalMass)*W.

Equations

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

noncomputable def EulerPacketRadiusPolynomial.radiusEnvelope (W : ℝ) : ℝ

Radius envelope, given by 18*W+2*requiredEnvelope W+meanEnvelope W+gradeEnvelope W*(1+terminalEnvelope W).

Equations

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

noncomputable def EulerPacketRadiusPolynomial.radiusPolynomial : Polynomial ℝ

Radius polynomial as an element of Polynomial ℝ.

Equations

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

theorem EulerPacketRadiusPolynomial.radiusPolynomial_eval (W : ℝ) : Polynomial.eval W radiusPolynomial = radiusEnvelope W

noncomputable def EulerPacketRadiusPolynomial.radiusConstant : ℝ

Radius constant, given by coefficientCost radiusPolynomial.

Equations

• EulerPacketRadiusPolynomial.radiusConstant = EulerPolynomialCost.coefficientCost EulerPacketRadiusPolynomial.radiusPolynomial

noncomputable def EulerPacketRadiusPolynomial.radiusPower : ℕ

Radius power, given by radiusPolynomial.natDegree.

Equations

• EulerPacketRadiusPolynomial.radiusPower = EulerPacketRadiusPolynomial.radiusPolynomial.natDegree

theorem EulerPacketRadiusPolynomial.radiusConstant_pos : 0 < radiusConstant

theorem EulerPacketRadiusPolynomial.radiusEnvelope_power (W : ℝ) (hW : 1 ≤ W) : radiusEnvelope W ≤ radiusConstant * W ^ radiusPower