English
Let f be a continuous multilinear map as above and e the embedding of α into ι. For any x: ι → E_i, the norm of the iteratedFDerivComponent is bounded above by the operator norm of f times the product of norms of x_i, raised to the power card(ι) − card(α).
Русский
Пусть f — непрерывное многолинейное отображение, а e — вложение α в ι. Для любого x: ι → E_i, нормa iteratedFDerivComponent удовлетворяет неравенству:
‖f.iteratedFDerivComponent e (x ·)‖ ≤ ‖f‖ · ‖x‖^{|ι| − |α|}.
LaTeX
$$$\|f\iteratedFDerivComponent e (x)\| \leq \|f\| \cdot \|x\|^{|ι| - |α|}$$$
Lean4
theorem norm_iteratedFDerivComponent_le {α : Type*} [Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι}
(e : α ≃ s) [DecidablePred (· ∈ s)] (x : (i : ι) → E₁ i) :
‖f.iteratedFDerivComponent e (x ·)‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α) :=
calc
‖f.iteratedFDerivComponent e (fun i ↦ x i)‖ ≤ ‖f.iteratedFDerivComponent e‖ * ∏ i : { a : ι // a ∉ s }, ‖x i‖ :=
ContinuousMultilinearMap.le_opNorm _ _
_ ≤ ‖f‖ * ∏ _i : { a : ι // a ∉ s }, ‖x‖ := by
gcongr
· exact MultilinearMap.mkContinuousMultilinear_norm_le _ (norm_nonneg _) _
· exact norm_le_pi_norm _ _
_ = ‖f‖ * ‖x‖ ^ (Fintype.card { a : ι // a ∉ s }) := by rw [prod_const, card_univ]
_ = ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α) := by simp [Fintype.card_congr e]
