Theorem: norm_iteratedFDerivWithin_prod_le
Proof state before:
case insert
𝕜 : 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'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Nat.choose n ↑m * Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Tactic:
rw [this, Nat.cast_mul]
Proof state after:
case insert
𝕜 : 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'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖) =
    ↑(Nat.choose n ↑m) * ↑(Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)