Supplementary lemmas for iterated derivatives

This file contains chain rules that are useful in the exponential-sums development but are not currently available in Mathlib in the required two-set form.

theorem Expdb.iteratedDerivWithin_comp_affine_of_mapsTo {f : ℝ → ℝ} {s t : Set ℝ} {x c d : ℝ} {n : ℕ} (hf : ContDiffOn ℝ (↑n) f t) (hs : UniqueDiffOn ℝ s) (ht : UniqueDiffOn ℝ t) (hx : x ∈ s) (hst : Set.MapsTo (fun (y : ℝ) => c * y + d) s t) : iteratedDerivWithin n (fun (y : ℝ) => f (c * y + d)) s x = c ^ n * iteratedDerivWithin n f t (c * x + d)

Iterated derivatives of a function precomposed with an affine map. Unlike Mathlib's iteratedDerivWithin_comp_const_smul, the domain and codomain sets may be different.