𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.1266934
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 : ℕ
x : E
⊢ ‖↑(changeOriginSeries p k l) fun x_1 => x‖₊ ≤ (∑' (x : { s // Finset.card s = l }), ‖p (k + l)‖₊) * ∏ _i : Fin l, ‖x‖₊
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.1266934
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 : ℕ
x : E
⊢ ‖↑(changeOriginSeries p k l) fun x_1 => x‖₊ ≤ ∑' (x_1 : { s // Finset.card s = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l
rw [NNReal.tsum_mul_right, ← Fin.prod_const]
no goals
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.1266934
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 : ℕ
x : E
⊢ ‖↑(changeOriginSeries p k l) fun x_1 => x‖₊ ≤ (∑' (x : { s // Finset.card s = l }), ‖p (k + l)‖₊) * ∏ _i : Fin l, ‖x‖₊
exact (p.changeOriginSeries k l).le_of_op_nnnorm_le _ (p.nnnorm_changeOriginSeries_le_tsum _ _)