norm_iteratedFDeriv_le — Mathlib

English

For f and x, the norm of iteratedFDeriv n f at x is bounded by a factorial factor, the norm of f, and a power of ‖x‖ depending on the arity n and the number of slots ι.

Русский

Для f и x нормa итеративного дифференциала ограничена факториалом, нормой f и степенью ‖x‖ в зависимости от n и количества слотов.

LaTeX

$$$\|\operatorname{iteratedFDeriv}_{n} f (x)\| \le \operatorname{descFactorial}(|ι|, n) \cdot \|f\| \cdot \|x\|^{|ι| - n}$$$

Lean4

theorem norm_iteratedFDeriv_le (n : ℕ) (x : (i : ι) → E i) :
    ‖iteratedFDeriv 𝕜 n f x‖ ≤ Nat.descFactorial (Fintype.card ι) n * ‖f‖ * ‖x‖ ^ (Fintype.card ι - n) :=
  by
  rw [f.iteratedFDeriv_eq]
  exact f.norm_iteratedFDeriv_le' n x

Похожие утверждения