Theorem: norm_iteratedFDeriv_prod_le (ForML/FDerivProd.lean)

State before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
u : Finset ι
f : ι → E → A'
N : ℕ∞
hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun x => ∏ j in u, f j x) x‖ ≤
    ∑ p in Finset.sym u n, ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖
Tactic:
simpa [iteratedFDerivWithin_univ] using
  norm_iteratedFDerivWithin_prod_le (fun i hi ↦ (hf i hi).contDiffOn) uniqueDiffOn_univ trivial hn
State after:
no goals