Joint monotonicity and genuine polynomial formulas for fixed-order coefficient and pressure constants. These give uniform parent-scale bounds.

theorem EulerParameterWordGevrey.sobolevCoefficientAmplitude_mono_all {ι : Type u_1} [Fintype ι] (q : ℕ) {R C S D : ℝ} (hR : 0 ≤ R) (hC : 0 ≤ C) (hRS : R ≤ S) (hCD : C ≤ D) : sobolevCoefficientAmplitude ι q R C ≤ sobolevCoefficientAmplitude ι q S D

noncomputable def EulerParameterWordGevrey.coefficientPolynomial (q : ℕ) (R C : Polynomial ℝ) : Polynomial ℝ

Coefficient polynomial, given by (2 : Polynomial ℝ)^q*C*∑ k ∈ range (q+1), (16*R)^k*Polynomial.C ((k.factorial : ℝ)^2).

Equations

• EulerParameterWordGevrey.coefficientPolynomial q R C = 2 ^ q * C * ∑ k ∈ Finset.range (q + 1), (16 * R) ^ k * Polynomial.C (↑k.factorial ^ 2)

theorem EulerParameterWordGevrey.coefficientPolynomial_eval (q : ℕ) (R C : Polynomial ℝ) (x : ℝ) : Polynomial.eval x (coefficientPolynomial q R C) = sobolevCoefficientAmplitude (Fin 4) q (Polynomial.eval x R) (Polynomial.eval x C)

theorem EulerCoefficientJetPressureBounds.productCost_mono {B C : ℝ} (hBC : B ≤ C) (q : ℕ) : productCost B q ≤ productCost C q

theorem EulerCoefficientJetPressureBounds.pressureCost_mono {c d B C : ℝ} (hc : 0 < c) (hd : 0 < d) (hB : 0 ≤ B) (hci : c⁻¹ ≤ d⁻¹) (hBC : B ≤ C) (q : ℕ) : pressureCost c B q ≤ pressureCost d C q

def EulerCoefficientJetPressureBounds.productPolynomial (B : Polynomial ℝ) : ℕ → Polynomial ℝ

Product polynomial as an element of ℕ → Polynomial ℝ | 0 => B | q+1 => B+8*productPolynomial B q.

Equations

• EulerCoefficientJetPressureBounds.productPolynomial B 0 = B
• EulerCoefficientJetPressureBounds.productPolynomial B q.succ = B + 8 * EulerCoefficientJetPressureBounds.productPolynomial B q

def EulerCoefficientJetPressureBounds.pressurePolynomial (i B : Polynomial ℝ) : ℕ → Polynomial ℝ

Pressure polynomial as an element of ℕ → Polynomial ℝ | 0 => i | q+1 => i+4*(pressurePolynomial i B q*(1+productPolynomial B q*pressurePolynomial i B q)).

Equations

• One or more equations did not get rendered due to their size.
• EulerCoefficientJetPressureBounds.pressurePolynomial i B 0 = i

theorem EulerCoefficientJetPressureBounds.productPolynomial_eval (B : Polynomial ℝ) (q : ℕ) (x : ℝ) : Polynomial.eval x (productPolynomial B q) = productCost (Polynomial.eval x B) q

theorem EulerCoefficientJetPressureBounds.pressurePolynomial_eval (i B : Polynomial ℝ) (q : ℕ) (x : ℝ) : Polynomial.eval x (pressurePolynomial i B q) = pressureCost (Polynomial.eval x i)⁻¹ (Polynomial.eval x B) q