English
An auxiliary estimate for the growth of derivatives of a composition under factorial scaling.
Русский
Вспомогательная оценка быстроты роста производных композиции.
LaTeX
$$$\displaystyle \| \operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (g \circ f) s x \| \le n! \cdot C \cdot D^n$$$
Lean4
theorem norm_iteratedFDerivWithin_prod_le [DecidableEq ι] [NormOneClass A'] {u : Finset ι} {f : ι → E → A'}
{N : WithTop ℕ∞} (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) (hs : UniqueDiffOn 𝕜 s) {x : E} (hx : x ∈ s) {n : ℕ}
(hn : n ≤ N) :
‖iteratedFDerivWithin 𝕜 n (∏ j ∈ u, f j ·) s x‖ ≤
∑ p ∈ u.sym n, (p : Multiset ι).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j p) (f j) s x‖ :=
by
induction u using Finset.induction generalizing n with
| empty =>
cases n with
| zero => simp [Sym.eq_nil_of_card_zero]
| succ n => simp [iteratedFDerivWithin_succ_const]
| insert i u hi IH =>
conv => lhs; simp only [Finset.prod_insert hi]
simp only [Finset.mem_insert, forall_eq_or_imp] at hf
refine le_trans (norm_iteratedFDerivWithin_mul_le hf.1 (contDiffOn_prod hf.2) hs hx hn) ?_
rw [← Finset.sum_coe_sort (Finset.sym _ _)]
rw [Finset.sum_equiv (Finset.symInsertEquiv hi) (t := Finset.univ) (g :=
(fun v ↦ v.multinomial * ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (v.count j) (f j) s x‖) ∘
Sym.toMultiset ∘ Subtype.val ∘ (Finset.symInsertEquiv hi).symm)
(by simp) (by simp only [← comp_apply (g := Finset.symInsertEquiv hi), comp_assoc]; simp)]
rw [← Finset.univ_sigma_univ, Finset.sum_sigma, Finset.sum_range]
simp only [comp_apply, Finset.symInsertEquiv_symm_apply_coe]
refine Finset.sum_le_sum ?_
intro m _
specialize IH hf.2 (n := n - m) (le_trans (by exact_mod_cast n.sub_le m) hn)
grw [IH]
rw [Finset.mul_sum, ← Finset.sum_coe_sort]
refine Finset.sum_le_sum ?_
simp only [Finset.mem_univ, forall_true_left, Subtype.forall, Finset.mem_sym_iff]
intro p hp
refine le_of_eq ?_
rw [Finset.prod_insert hi]
have hip : i ∉ p := mt (hp i) hi
rw [Sym.count_coe_fill_self_of_notMem hip, Sym.multinomial_coe_fill_of_notMem hip]
suffices
∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j p) (f j) s x‖ =
∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j (Sym.fill i m p)) (f j) s x‖
by
rw [this, Nat.cast_mul]
ring
refine Finset.prod_congr rfl ?_
intro j hj
have hji : j ≠ i := mt (· ▸ hj) hi
rw [Sym.count_coe_fill_of_ne hji]
