The actual inverse estimate at a fixed Sobolev order

Differentiate the genuine equation once at each of finitely many base indices. The resulting constant is a fixed polynomial recursion in the ordinary inverse norm and the finite coefficient-jet bound. It does not depend on any external derivative order or factorial shift.

def EulerParameterWordGevrey.sobolevInverseCost (I B : ℝ) : ℕ → ℝ

A fixed finite recursion of polynomial base-order inverse constants.

Equations

• EulerParameterWordGevrey.sobolevInverseCost I B 0 = I
• EulerParameterWordGevrey.sobolevInverseCost I B q.succ = I + EulerParameterWordGevrey.sobolevInverseCost I B q + 2 ^ q * B * EulerParameterWordGevrey.sobolevInverseCost I B q ^ 2

theorem EulerParameterWordGevrey.sobolevInverseCost_nonneg (I B : ℝ) (hI : 0 ≤ I) (hB : 0 ≤ B) (q : ℕ) : 0 ≤ sobolevInverseCost I B q

theorem EulerParameterWordGevrey.baseSize_inverse_bound {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (A : P → E →L[ℝ] E) (hA : ContDiff ℝ (↑⊤) A) (x : P) (inverse : E →L[ℝ] E) (hleft : ∀ (v : E), inverse ((A x) v) = v) (I B : ℝ) (hinv : ‖inverse‖ ≤ I) (q : ℕ) (u f : P → E) : ContDiff ℝ (↑⊤) u → ContDiff ℝ (↑⊤) f → (∀ (y : P), (A y) (u y) = f y) → baseSize directions q A x ≤ B → baseSize directions q u x ≤ sobolevInverseCost I B q * baseSize directions q f x

Fixed-order Sobolev boundedness of an actual inverse equation. Every derivative is an ordinary derivative of the original smooth functions.