𝕜 : Type u_3
E : Type u_2
F : Type u_1
G : Type ?u.1230559
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x✝ y✝ : E
r R : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : Finset.card s = l
x y : E
⊢ ‖↑(↑(changeOriginSeriesTerm p k l s hs) fun x_1 => x) fun x => y‖₊ ≤
    (‖changeOriginSeriesTerm p k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊) * ∏ _i : Fin k, ‖y‖₊
𝕜 : Type u_3
E : Type u_2
F : Type u_1
G : Type ?u.1230559
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x✝ y✝ : E
r R : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : Finset.card s = l
x y : E
⊢ ‖↑(↑(changeOriginSeriesTerm p k l s hs) fun x_1 => x) fun x => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k
rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const]
case h
𝕜 : Type u_3
E : Type u_2
F : Type u_1
G : Type ?u.1230559
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x✝ y✝ : E
r R : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : Finset.card s = l
x y : E
⊢ ‖↑(changeOriginSeriesTerm p k l s hs) fun x_1 => x‖₊ ≤ ‖changeOriginSeriesTerm p k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊
𝕜 : Type u_3
E : Type u_2
F : Type u_1
G : Type ?u.1230559
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x✝ y✝ : E
r R : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : Finset.card s = l
x y : E
⊢ ‖↑(↑(changeOriginSeriesTerm p k l s hs) fun x_1 => x) fun x => y‖₊ ≤
    (‖changeOriginSeriesTerm p k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊) * ∏ _i : Fin k, ‖y‖₊
apply ContinuousMultilinearMap.le_of_op_nnnorm_le
no goals
case h
𝕜 : Type u_3
E : Type u_2
F : Type u_1
G : Type ?u.1230559
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x✝ y✝ : E
r R : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : Finset.card s = l
x y : E
⊢ ‖↑(changeOriginSeriesTerm p k l s hs) fun x_1 => x‖₊ ≤ ‖changeOriginSeriesTerm p k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊
apply ContinuousMultilinearMap.le_op_nnnorm