Iterated derivative of product

Stream: Is there code for X?

[Vincent Beffara]

Do we have this (under the right assumptions of course)?

theorem blo (f g : ℝ → ℂ) (n : ℕ) : iteratedDeriv n (fun x => f x * g x) = fun x =>
    ∑ k in Finset.Icc 0 n, ((n.choose k) * iteratedDeriv k f x * iteratedDeriv (n - k) g x) := by sorry

It is kind of hidden in the proof of docs#ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux

[Sébastien Gouëzel]

I don't think we have it, and we definitely should (for a general bilinear form, then specialized to multiplication). Note however that if you just need to bound some integrals, a bound (like the one you mention or the one given by docs#norm_iteratedFDeriv_mul_le) could be enough for your needs.