Monotonicity of the explicit finite-order inverse polynomials. These lemmas replace actual operator constants by source-scale upper bounds.

theorem EulerParameterWordGevrey.sobolevInverseCost_mono {I J B C : ℝ} (hI : 0 ≤ I) (hB : 0 ≤ B) (hIJ : I ≤ J) (hBC : B ≤ C) (q : ℕ) : sobolevInverseCost I B q ≤ sobolevInverseCost J C q

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

theorem EulerParameterWordGevrey.inverseBlockCost_mono {ι : Type u_1} [Fintype ι] (q : ℕ) {I J R C C' D D' : ℝ} (hI : 0 ≤ I) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (hIJ : I ≤ J) (hCC : C ≤ C') (hDD : D ≤ D') : inverseBlockCost ι q I R C D ≤ inverseBlockCost ι q J R C' D'