English
For any finite α ⊆ ι and equiv e: α ≃ s, the norm of the iterated derivative f.iteratedDeriv at x is bounded by the product of factorial-type bound and operator norm of f times a power of ‖x‖.
Русский
Для любого конечного α ⊆ ι и эквивалента e: α ≃ s, норма итеративной производной f.iteratedDeriv удовлетворяет верхней границе, равной факториальному пределу отcard(ι) умноженному на ‖f‖ и на ‖x‖^{card(ι) − card(α)}.
LaTeX
$$$\|f.iteratedFDeriv k x\| \leq {\operatorname{descFactorial}( |ι|, k )} \cdot \|f\| \cdot \|x\|^{|ι| - k}$$$
Lean4
/-- Controlling the norm of `f.iteratedFDeriv` when `f` is continuous multilinear. For the same
bound on the iterated derivative of `f` in the calculus sense,
see `ContinuousMultilinearMap.norm_iteratedFDeriv_le`. -/
theorem norm_iteratedFDeriv_le' (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i) :
‖f.iteratedFDeriv k x‖ ≤ Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
classical
calc
‖f.iteratedFDeriv k x‖
_ ≤ ∑ e : Fin k ↪ ι, ‖iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)‖ := (norm_sum_le _ _)
_ ≤ ∑ _ : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) :=
by
gcongr with e _
simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x
_ = Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by simp [card_univ, mul_assoc]
