have hg_bound := hg.bound_forall_range (n + 1)
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k
D : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace ℝ D
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : D → E →L[ℝ] F
hf : HasTemperateGrowth f
g : D → E
hg : HasTemperateGrowth g
n : ℕ
hf_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i f x‖ ≤ C * (1 + ‖x‖) ^ k
hg_bound : ∃ k C, 0 ≤ C ∧ ∀ i ∈ Finset.range (n + 1), ∀ (x : D), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (fun x => (f x) (g x)) x‖ ≤ C * (1 + ‖x‖) ^ k