∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} {K : WithTop ℕ∞} {C : ℝ},
  ContDiff ℝ K f →
    ∀ {n k : ℕ},
      ↑k ≤ K →
        ∀ {v : V},
          (∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C) →
            ‖iteratedFDeriv ℝ k (fun v => VectorFourier.fourierPowSMulRight L f v n) v‖ ≤
              (2 * Real.pi) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C