mathlib3

91862a60 - feat(analysis/calculus/cont_diff): bound for the iterated derivative of a product (#18632)

feat(analysis/calculus/cont_diff): bound for the iterated derivative of a product (#18632) We show that `‖D^n (x ↦ B (f x) (g x))‖ ≤ ‖B‖ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖` for a general continuous bilinear map `B`, and specialize this inequality to the case of the product of two functions. This is a first step to control the norm of the iterated derivative of a composition.